Theorem relopabi 5116

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 4498	. . . 4 |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3	1, 2	eqtri 2483	. . 3 |- A = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
4		vex 3109	. . . . . . . 8 |- x e. _V
5		vex 3109	. . . . . . . 8 |- y e. _V
6	4, 5	opelvv 5035	. . . . . . 7 |- <. x , y >. e. ( _V X. _V )
7		eleq1 2526	. . . . . . 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 463	. . . . 5 |- ( ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
10	9	exlimivv 1728	. . . 4 |- ( E. x E. y ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
11	10	abssi 3561	. . 3 |- { z | E. x E. y ( z = <. x , y >. /\ ph ) } C_ ( _V X. _V )
12	3, 11	eqsstri 3519	. 2 |- A C_ ( _V X. _V )
13		df-rel 4995	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
14	12, 13	mpbir 209	1 |- Rel A

Syntax hints:   /\ wa 367   = wceq 1398   E.wex 1617   e. wcel 1823   {cab 2439   _Vcvv 3106   C_ wss 3461   <.cop 4022   {copab 4496   X. cxp 4986   Rel wrel 4993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-opab 4498  df-xp 4994  df-rel 4995

This theorem is referenced by:  relopab  5117  mptrel  5118  reli  5119  rele  5120  relcnv  5362  cotrg  5366  relco  5488  reloprab  6317  reldmoprab  6360  relrpss  6554  eqer  7336  ecopover  7407  relen  7514  reldom  7515  relfsupp  7823  relwdom  7984  fpwwe2lem2  8999  fpwwe2lem3  9000  fpwwe2lem6  9002  fpwwe2lem7  9003  fpwwe2lem9  9005  fpwwe2lem11  9007  fpwwe2lem12  9008  fpwwe2lem13  9009  fpwwelem  9012  climrel  13397  rlimrel  13398  brstruct  14724  sscrel  15301  gaorber  16545  sylow2a  16838  efgrelexlemb  16967  efgcpbllemb  16972  rellindf  19010  tpsexOLD  19587  2ndcctbss  20122  refrel  20175  vitalilem1  22183  lgsquadlem1  23827  lgsquadlem2  23828  reluhgra  24496  relushgra  24497  relumgra  24516  reluslgra  24536  relusgra  24537  iscusgra0  24659  cusgrasize  24680  erclwwlkrel  25012  erclwwlknrel  25024  frisusgrapr  25193  relrngo  25577  drngoi  25607  isdivrngo  25631  vcrel  25638  h2hlm  26095  hlimi  26303  relmntop  28236  relae  28449  fnerel  30396  filnetlem3  30438  brabg2  30446  heiborlem3  30549  heiborlem4  30550  isdrngo1  30599  riscer  30631  prter1  30860  prter3  30863  reldvds  31461  relfusgra  32795  rellininds  33298