Theorem relopabi 4980

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 4366	. . . 4 |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3	1, 2	eqtri 2463	. . 3 |- A = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
4		vex 2990	. . . . . . . 8 |- x e. _V
5		vex 2990	. . . . . . . 8 |- y e. _V
6	4, 5	opelvv 4900	. . . . . . 7 |- <. x , y >. e. ( _V X. _V )
7		eleq1 2503	. . . . . . 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 1689	. . . 4 |- ( E. x E. y ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
11	10	abssi 3442	. . 3 |- { z | E. x E. y ( z = <. x , y >. /\ ph ) } C_ ( _V X. _V )
12	3, 11	eqsstri 3401	. 2 |- A C_ ( _V X. _V )
13		df-rel 4862	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
14	12, 13	mpbir 209	1 |- Rel A

Syntax hints:   /\ wa 369   = wceq 1369   E.wex 1586   e. wcel 1756   {cab 2429   _Vcvv 2987   C_ wss 3343   <.cop 3898   {copab 4364   X. cxp 4853   Rel wrel 4860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pr 4546

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-rab 2739  df-v 2989  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-opab 4366  df-xp 4861  df-rel 4862

This theorem is referenced by:  relopab  4981  reli  4982  rele  4983  relcnv  5221  cotr  5225  relco  5351  reloprab  6149  reldmoprab  6190  relrpss  6376  eqer  7149  ecopover  7219  relen  7330  reldom  7331  relfsupp  7637  fsuppimp  7641  wemapso2  7783  relwdom  7796  fpwwe2lem2  8814  fpwwe2lem3  8815  fpwwe2lem6  8817  fpwwe2lem7  8818  fpwwe2lem9  8820  fpwwe2lem11  8822  fpwwe2lem12  8823  fpwwe2lem13  8824  fpwwelem  8827  fpwwe  8828  climrel  12985  rlimrel  12986  brstruct  14197  sscrel  14741  gaorber  15841  sylow2a  16133  efgrelexlema  16261  efgrelexlemb  16262  efgcpbllemb  16267  rellindf  18252  tpsexOLD  18539  2ndcctbss  19074  vitalilem1  21103  lgsquadlem1  22708  lgsquadlem2  22709  reluhgra  23250  relumgra  23263  reluslgra  23282  relusgra  23283  iscusgra0  23380  cusgrasize  23401  relrngo  23879  drngoi  23909  isdivrngo  23933  vcrel  23940  h2hlm  24397  hlimi  24605  relae  26671  mptrel  27594  fnerel  28558  refrel  28569  filnetlem3  28620  brabg2  28628  heiborlem3  28731  heiborlem4  28732  isdrngo1  28781  riscer  28813  prter1  29043  prter3  29046  erclwwlkrel  30499  erclwwlknrel  30515  frisusgrapr  30602  rellininds  30996