Theorem relopabi 4916

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 4421	. . . 4 |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3	1, 2	eqtri 2445	. . 3 |- A = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
4		vex 3020	. . . . . . . 8 |- x e. _V
5		vex 3020	. . . . . . . 8 |- y e. _V
6	4, 5	opelvv 4838	. . . . . . 7 |- <. x , y >. e. ( _V X. _V )
7		eleq1 2489	. . . . . . 7 |- ( z = <. x , y >. -> ( z e. ( _V X. _V ) <-> <. x , y >. e. ( _V X. _V ) ) )
8	6, 7	mpbiri 236	. . . . . 6 |- ( z = <. x , y >. -> z e. ( _V X. _V ) )
9	8	adantr 466	. . . . 5 |- ( ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
10	9	exlimivv 1771	. . . 4 |- ( E. x E. y ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
11	10	abssi 3474	. . 3 |- { z | E. x E. y ( z = <. x , y >. /\ ph ) } C_ ( _V X. _V )
12	3, 11	eqsstri 3432	. 2 |- A C_ ( _V X. _V )
13		df-rel 4798	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
14	12, 13	mpbir 212	1 |- Rel A

Syntax hints:   /\ wa 370   = wceq 1437   E.wex 1657   e. wcel 1872   {cab 2409   _Vcvv 3017   C_ wss 3374   <.cop 3942   {copab 4419   X. cxp 4789   Rel wrel 4796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pr 4598

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-opab 4421  df-xp 4797  df-rel 4798

This theorem is referenced by:  relopab  4917  mptrel  4918  reli  4919  rele  4920  relcnv  5164  cotrg  5168  relco  5290  reloprab  6291  reldmoprab  6334  relrpss  6525  eqer  7346  ecopover  7417  relen  7524  reldom  7525  relfsupp  7833  relwdom  8029  fpwwe2lem2  9003  fpwwe2lem3  9004  fpwwe2lem6  9006  fpwwe2lem7  9007  fpwwe2lem9  9009  fpwwe2lem11  9011  fpwwe2lem12  9012  fpwwe2lem13  9013  fpwwelem  9016  climrel  13494  rlimrel  13495  brstruct  15067  sscrel  15656  gaorber  16900  sylow2a  17209  efgrelexlemb  17338  efgcpbllemb  17343  rellindf  19303  2ndcctbss  20407  refrel  20460  vitalilem1  22503  lgsquadlem1  24219  lgsquadlem2  24220  reluhgra  24958  relushgra  24959  relumgra  24978  reluslgra  24998  relusgra  24999  iscusgra0  25122  cusgrasize  25143  erclwwlkrel  25475  erclwwlknrel  25487  frisusgrapr  25656  relrngo  26042  drngoi  26072  isdivrngo  26096  vcrel  26103  h2hlm  26570  hlimi  26778  relmntop  28775  relae  29010  fnerel  30938  filnetlem3  30980  brabg2  31949  heiborlem3  32052  heiborlem4  32053  isdrngo1  32102  riscer  32134  prter1  32362  prter3  32365  reldvds  36577  relsubgr  39078  relfusgra  39326  rellininds  39829