Theorem relopabi 5245

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

Hypothesis

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

Assertion

Ref	Expression
relopabi	|- Rel A

Proof of Theorem relopabi

Dummy variables z u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relopabi.1	. . . . . . . 8 |- A = { <. x , y >. | ph }
2		df-opab 4713	. . . . . . . 8 |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3	1, 2	eqtri 2644	. . . . . . 7 |- A = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
4	3	abeq2i 2735	. . . . . 6 |- ( z e. A <-> E. x E. y ( z = <. x , y >. /\ ph ) )
5		simpl 473	. . . . . . 7 |- ( ( z = <. x , y >. /\ ph ) -> z = <. x , y >. )
6	5	2eximi 1763	. . . . . 6 |- ( E. x E. y ( z = <. x , y >. /\ ph ) -> E. x E. y z = <. x , y >. )
7	4, 6	sylbi 207	. . . . 5 |- ( z e. A -> E. x E. y z = <. x , y >. )
8		ax6evr 1942	. . . . . . . . . 10 |- E. u y = u
9		pm3.21 464	. . . . . . . . . . 11 |- ( <. x , y >. = z -> ( y = u -> ( y = u /\ <. x , y >. = z ) ) )
10	9	eximdv 1846	. . . . . . . . . 10 |- ( <. x , y >. = z -> ( E. u y = u -> E. u ( y = u /\ <. x , y >. = z ) ) )
11	8, 10	mpi 20	. . . . . . . . 9 |- ( <. x , y >. = z -> E. u ( y = u /\ <. x , y >. = z ) )
12		opeq2 4403	. . . . . . . . . . 11 |- ( y = u -> <. x , y >. = <. x , u >. )
13		eqtr2 2642	. . . . . . . . . . . 12 |- ( ( <. x , y >. = <. x , u >. /\ <. x , y >. = z ) -> <. x , u >. = z )
14	13	eqcomd 2628	. . . . . . . . . . 11 |- ( ( <. x , y >. = <. x , u >. /\ <. x , y >. = z ) -> z = <. x , u >. )
15	12, 14	sylan 488	. . . . . . . . . 10 |- ( ( y = u /\ <. x , y >. = z ) -> z = <. x , u >. )
16	15	eximi 1762	. . . . . . . . 9 |- ( E. u ( y = u /\ <. x , y >. = z ) -> E. u z = <. x , u >. )
17	11, 16	syl 17	. . . . . . . 8 |- ( <. x , y >. = z -> E. u z = <. x , u >. )
18	17	eqcoms 2630	. . . . . . 7 |- ( z = <. x , y >. -> E. u z = <. x , u >. )
19	18	2eximi 1763	. . . . . 6 |- ( E. x E. y z = <. x , y >. -> E. x E. y E. u z = <. x , u >. )
20		excomim 2043	. . . . . 6 |- ( E. x E. y E. u z = <. x , u >. -> E. y E. x E. u z = <. x , u >. )
21	19, 20	syl 17	. . . . 5 |- ( E. x E. y z = <. x , y >. -> E. y E. x E. u z = <. x , u >. )
22		vex 3203	. . . . . . . . . 10 |- x e. _V
23		vex 3203	. . . . . . . . . 10 |- u e. _V
24	22, 23	pm3.2i 471	. . . . . . . . 9 |- ( x e. _V /\ u e. _V )
25	24	jctr 565	. . . . . . . 8 |- ( z = <. x , u >. -> ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
26	25	2eximi 1763	. . . . . . 7 |- ( E. x E. u z = <. x , u >. -> E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
27		df-xp 5120	. . . . . . . . 9 |- ( _V X. _V ) = { <. x , u >. | ( x e. _V /\ u e. _V ) }
28		df-opab 4713	. . . . . . . . 9 |- { <. 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 2644	. . . . . . . 8 |- ( _V X. _V ) = { z | E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) }
30	29	abeq2i 2735	. . . . . . 7 |- ( z e. ( _V X. _V ) <-> E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
31	26, 30	sylibr 224	. . . . . 6 |- ( E. x E. u z = <. x , u >. -> z e. ( _V X. _V ) )
32	31	eximi 1762	. . . . 5 |- ( E. y E. x E. u z = <. x , u >. -> E. y z e. ( _V X. _V ) )
33	7, 21, 32	3syl 18	. . . 4 |- ( z e. A -> E. y z e. ( _V X. _V ) )
34		ax5e 1841	. . . 4 |- ( E. y z e. ( _V X. _V ) -> z e. ( _V X. _V ) )
35	33, 34	syl 17	. . 3 |- ( z e. A -> z e. ( _V X. _V ) )
36	35	ssriv 3607	. 2 |- A C_ ( _V X. _V )
37		df-rel 5121	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
38	36, 37	mpbir 221	1 |- Rel A

Syntax hints:   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   _Vcvv 3200   C_ wss 3574   <.cop 4183   {copab 4712   X. cxp 5112   Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120  df-rel 5121

This theorem is referenced by:  relopab  5247  mptrel  5248  reli  5249  rele  5250  relcnv  5503  cotrg  5507  relco  5633  brfvopabrbr  6279  reloprab  6702  reldmoprab  6745  relrpss  6938  eqer  7777  eqerOLD  7778  ecopover  7851  ecopoverOLD  7852  relen  7960  reldom  7961  relfsupp  8277  relwdom  8471  fpwwe2lem2  9454  fpwwe2lem3  9455  fpwwe2lem6  9457  fpwwe2lem7  9458  fpwwe2lem9  9460  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwelem  9467  climrel  14223  rlimrel  14224  brstruct  15866  sscrel  16473  gaorber  17741  sylow2a  18034  efgrelexlemb  18163  efgcpbllemb  18168  rellindf  20147  2ndcctbss  21258  refrel  21311  vitalilem1  23376  vitalilem1OLD  23377  lgsquadlem1  25105  lgsquadlem2  25106  relsubgr  26161  erclwwlksrel  26931  erclwwlksnrel  26943  vcrel  27415  h2hlm  27837  hlimi  28045  relmntop  30068  relae  30303  dmscut  31918  fnerel  32333  filnetlem3  32375  brabg2  33510  heiborlem3  33612  heiborlem4  33613  relrngo  33695  isdivrngo  33749  drngoi  33750  isdrngo1  33755  riscer  33787  prter1  34164  prter3  34167  reldvds  38514  nelbrim  41292  rellininds  42232