Theorem relopabi 4977

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 4475	. . . 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 3059	. . . . . . . 8 |- x e. _V
5		vex 3059	. . . . . . . 8 |- y e. _V
6	4, 5	opelvv 4899	. . . . . . 7 |- <. x , y >. e. ( _V X. _V )
7		eleq1 2527	. . . . . . 7 |- ( z = <. x , y >. -> ( z e. ( _V X. _V ) <-> <. x , y >. e. ( _V X. _V ) ) )
8	6, 7	mpbiri 241	. . . . . 6 |- ( z = <. x , y >. -> z e. ( _V X. _V ) )
9	8	adantr 471	. . . . 5 |- ( ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
10	9	exlimivv 1788	. . . 4 |- ( E. x E. y ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
11	10	abssi 3515	. . 3 |- { z | E. x E. y ( z = <. x , y >. /\ ph ) } C_ ( _V X. _V )
12	3, 11	eqsstri 3473	. 2 |- A C_ ( _V X. _V )
13		df-rel 4859	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
14	12, 13	mpbir 214	1 |- Rel A

Syntax hints:   /\ wa 375   = wceq 1454   E.wex 1673   e. wcel 1897   {cab 2447   _Vcvv 3056   C_ wss 3415   <.cop 3985   {copab 4473   X. cxp 4850   Rel wrel 4857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-opab 4475  df-xp 4858  df-rel 4859

This theorem is referenced by:  relopab  4978  mptrel  4979  reli  4980  rele  4981  relcnv  5225  cotrg  5229  relco  5351  reloprab  6364  reldmoprab  6407  relrpss  6598  eqer  7421  ecopover  7492  relen  7599  reldom  7600  relfsupp  7910  relwdom  8106  fpwwe2lem2  9082  fpwwe2lem3  9083  fpwwe2lem6  9085  fpwwe2lem7  9086  fpwwe2lem9  9088  fpwwe2lem11  9090  fpwwe2lem12  9091  fpwwe2lem13  9092  fpwwelem  9095  climrel  13604  rlimrel  13605  brstruct  15177  sscrel  15766  gaorber  17010  sylow2a  17319  efgrelexlemb  17448  efgcpbllemb  17453  rellindf  19414  2ndcctbss  20518  refrel  20571  vitalilem1  22614  lgsquadlem1  24330  lgsquadlem2  24331  reluhgra  25069  relushgra  25070  relumgra  25089  reluslgra  25109  relusgra  25110  iscusgra0  25233  cusgrasize  25254  erclwwlkrel  25586  erclwwlknrel  25598  frisusgrapr  25767  relrngo  26153  drngoi  26183  isdivrngo  26207  vcrel  26214  h2hlm  26681  hlimi  26889  relmntop  28876  relae  29111  fnerel  31042  filnetlem3  31084  brabg2  32086  heiborlem3  32189  heiborlem4  32190  isdrngo1  32239  riscer  32271  prter1  32495  prter3  32498  reldvds  36707  relsubgr  39390  relfusgra  40007  rellininds  40508