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	2	preq1d	_1 = x /\ _2 = z -> _1, y = x, y
4	3	eleq1d	_1 = x /\ _2 = z -> (_1, y e. A <-> x, y e. A)
5		id	_2 = z -> _2 = z
6	5	anwr	_1 = x /\ _2 = z -> _2 = z
7	6	preq2d	_1 = x /\ _2 = z -> y, _2 = y, z
8	7	eleq1d	_1 = x /\ _2 = z -> (y, _2 e. B <-> y, z e. B)
9	4, 8	aneqd	_1 = x /\ _2 = z -> (_1, y e. A /\ y, _2 e. B <-> x, y e. A /\ y, z e. B)
10	9	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))
11	10	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))
12	11	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)
13	12	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)