Theorem relopabi 5126

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)

Hypothesis

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

Assertion

Ref	Expression
relopabi	|- Rel A

Proof of Theorem relopabi

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		relopabi.1	. . . 4 |- A = { <. x , y >. | ph }
2		df-opab 4506	. . . 4 |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3	1, 2	eqtri 2496	. . 3 |- A = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
4		vex 3116	. . . . . . . 8 |- x e. _V
5		vex 3116	. . . . . . . 8 |- y e. _V
6	4, 5	opelvv 5045	. . . . . . 7 |- <. x , y >. e. ( _V X. _V )
7		eleq1 2539	. . . . . . 7 |- ( z = <. x , y >. -> ( z e. ( _V X. _V ) <-> <. x , y >. e. ( _V X. _V ) ) )
8	6, 7	mpbiri 233	. . . . . 6 |- ( z = <. x , y >. -> z e. ( _V X. _V ) )
9	8	adantr 465	. . . . 5 |- ( ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
10	9	exlimivv 1699	. . . 4 |- ( E. x E. y ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
11	10	abssi 3575	. . 3 |- { z | E. x E. y ( z = <. x , y >. /\ ph ) } C_ ( _V X. _V )
12	3, 11	eqsstri 3534	. 2 |- A C_ ( _V X. _V )
13		df-rel 5006	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
14	12, 13	mpbir 209	1 |- Rel A

Syntax hints:   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   {cab 2452   _Vcvv 3113   C_ wss 3476   <.cop 4033   {copab 4504   X. cxp 4997   Rel wrel 5004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-opab 4506  df-xp 5005  df-rel 5006

This theorem is referenced by:  relopab  5127  reli  5128  rele  5129  relcnv  5372  cotrg  5376  relco  5503  reloprab  6326  reldmoprab  6369  relrpss  6563  eqer  7341  ecopover  7412  relen  7518  reldom  7519  relfsupp  7827  fsuppimp  7831  wemapso2  7975  relwdom  7988  fpwwe2lem2  9006  fpwwe2lem3  9007  fpwwe2lem6  9009  fpwwe2lem7  9010  fpwwe2lem9  9012  fpwwe2lem11  9014  fpwwe2lem12  9015  fpwwe2lem13  9016  fpwwelem  9019  fpwwe  9020  climrel  13274  rlimrel  13275  brstruct  14494  sscrel  15039  gaorber  16141  sylow2a  16435  efgrelexlema  16563  efgrelexlemb  16564  efgcpbllemb  16569  rellindf  18610  tpsexOLD  19187  2ndcctbss  19722  vitalilem1  21752  lgsquadlem1  23357  lgsquadlem2  23358  reluhgra  23970  relushgra  23971  relumgra  23990  reluslgra  24010  relusgra  24011  iscusgra0  24133  cusgrasize  24154  erclwwlkrel  24486  erclwwlknrel  24498  frisusgrapr  24667  relrngo  25055  drngoi  25085  isdivrngo  25109  vcrel  25116  h2hlm  25573  hlimi  25781  relmntop  27642  relae  27852  mptrel  28775  fnerel  29739  refrel  29750  filnetlem3  29801  brabg2  29809  heiborlem3  29912  heiborlem4  29913  isdrngo1  29962  riscer  29994  prter1  30224  prter3  30227  reldvds  30820  relfusgra  31892  rellininds  32117