Theorem relopabi

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021)

	Ref	Expression
Hypothesis	relopabi.1	|- A = { <. x , y >. | ph }
Assertion	relopabi	|- Rel A

Proof

Step	Hyp	Ref	Expression
1		relopabi.1	|- A = { <. x , y >. | ph }
2		df-opab	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3	1 2	eqtri	|- A = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
4	3	abeq2i	|- ( z e. A <-> E. x E. y ( z = <. x , y >. /\ ph ) )
5		simpl	|- ( ( z = <. x , y >. /\ ph ) -> z = <. x , y >. )
6	5	2eximi	|- ( E. x E. y ( z = <. x , y >. /\ ph ) -> E. x E. y z = <. x , y >. )
7	4 6	sylbi	|- ( z e. A -> E. x E. y z = <. x , y >. )
8		ax6evr	|- E. u y = u
9		pm3.21	|- ( <. x , y >. = z -> ( y = u -> ( y = u /\ <. x , y >. = z ) ) )
10	9	eximdv	|- ( <. x , y >. = z -> ( E. u y = u -> E. u ( y = u /\ <. x , y >. = z ) ) )
11	8 10	mpi	|- ( <. x , y >. = z -> E. u ( y = u /\ <. x , y >. = z ) )
12		opeq2	|- ( y = u -> <. x , y >. = <. x , u >. )
13		eqtr2	|- ( ( <. x , y >. = <. x , u >. /\ <. x , y >. = z ) -> <. x , u >. = z )
14	13	eqcomd	|- ( ( <. x , y >. = <. x , u >. /\ <. x , y >. = z ) -> z = <. x , u >. )
15	12 14	sylan	|- ( ( y = u /\ <. x , y >. = z ) -> z = <. x , u >. )
16	15	eximi	|- ( E. u ( y = u /\ <. x , y >. = z ) -> E. u z = <. x , u >. )
17	11 16	syl	|- ( <. x , y >. = z -> E. u z = <. x , u >. )
18	17	eqcoms	|- ( z = <. x , y >. -> E. u z = <. x , u >. )
19	18	2eximi	|- ( E. x E. y z = <. x , y >. -> E. x E. y E. u z = <. x , u >. )
20		excomim	|- ( E. x E. y E. u z = <. x , u >. -> E. y E. x E. u z = <. x , u >. )
21	19 20	syl	|- ( E. x E. y z = <. x , y >. -> E. y E. x E. u z = <. x , u >. )
22		vex	|- x e. _V
23		vex	|- u e. _V
24	22 23	pm3.2i	|- ( x e. _V /\ u e. _V )
25	24	jctr	|- ( z = <. x , u >. -> ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
26	25	2eximi	|- ( E. x E. u z = <. x , u >. -> E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
27		df-xp	|- ( _V X. _V ) = { <. x , u >. | ( x e. _V /\ u e. _V ) }
28		df-opab	|- { <. x , u >. | ( x e. _V /\ u e. _V ) } = { z | E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) }
29	27 28	eqtri	|- ( _V X. _V ) = { z | E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) }
30	29	abeq2i	|- ( z e. ( _V X. _V ) <-> E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
31	26 30	sylibr	|- ( E. x E. u z = <. x , u >. -> z e. ( _V X. _V ) )
32	31	eximi	|- ( E. y E. x E. u z = <. x , u >. -> E. y z e. ( _V X. _V ) )
33	7 21 32	3syl	|- ( z e. A -> E. y z e. ( _V X. _V ) )
34		ax5e	|- ( E. y z e. ( _V X. _V ) -> z e. ( _V X. _V ) )
35	33 34	syl	|- ( z e. A -> z e. ( _V X. _V ) )
36	35	ssriv	|- A C_ ( _V X. _V )
37		df-rel	|- ( Rel A <-> A C_ ( _V X. _V ) )
38	36 37	mpbir	|- Rel A