Theorem prco ≪ | index | src | ≫

theorem prco (A B: set) (x: nat) {y: nat} (z: nat):
  $ x, z e. A o> B <-> E. y (x, y e. A /\ y, z e. B) $;

Step	Hyp	Ref	Expression
1		id	_1 = x -> _1 = x
2	1	anwl	_1 = x /\ _2 = z -> _1 = x
3		eqidd	_1 = x /\ _2 = z -> y = y
4	2, 3	preqd	_1 = x /\ _2 = z -> _1, y = x, y
5		eqsidd	_1 = x /\ _2 = z -> A == A
6	4, 5	eleqd	_1 = x /\ _2 = z -> (_1, y e. A <-> x, y e. A)
7		id	_2 = z -> _2 = z
8	7	anwr	_1 = x /\ _2 = z -> _2 = z
9	3, 8	preqd	_1 = x /\ _2 = z -> y, _2 = y, z
10		eqsidd	_1 = x /\ _2 = z -> B == B
11	9, 10	eleqd	_1 = x /\ _2 = z -> (y, _2 e. B <-> y, z e. B)
12	6, 11	aneqd	_1 = x /\ _2 = z -> (_1, y e. A /\ y, _2 e. B <-> x, y e. A /\ y, z e. B)
13	12	exeqd	_1 = x /\ _2 = z -> (E. y (_1, y e. A /\ y, _2 e. B) <-> E. y (x, y e. A /\ y, z e. B))
14	13	elabed	_1 = x -> (z e. {_2 \| E. y (_1, y e. A /\ y, _2 e. B)} <-> E. y (x, y e. A /\ y, z e. B))
15	14	elsabe	x, z e. S\ _1, {_2 \| E. y (_1, y e. A /\ y, _2 e. B)} <-> E. y (x, y e. A /\ y, z e. B)
16	15	conv comp	x, z e. A o> B <-> E. y (x, y e. A /\ y, z e. B)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)