Theorem relopabi 5133

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

Hypothesis

Ref	Expression
relopabi.1

Assertion

Ref	Expression
relopabi

Proof of Theorem relopabi

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		relopabi.1	. . . 4
2		df-opab 4511	. . . 4
3	1, 2	eqtri 2486	. . 3
4		vex 3112	. . . . . . . 8
5		vex 3112	. . . . . . . 8
6	4, 5	opelvv 5051	. . . . . . 7
7		eleq1 2529	. . . . . . 7
8	6, 7	mpbiri 233	. . . . . 6
9	8	adantr 465	. . . . 5
10	9	exlimivv 1723	. . . 4
11	10	abssi 3574	. . 3
12	3, 11	eqsstri 3533	. 2
13		df-rel 5011	. 2
14	12, 13	mpbir 209	1

Syntax hints:  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  {cab 2442  cvv 3109  C_wss 3475  <.cop 4035  {copab 4509  X.cxp 5002  Relwrel 5009

This theorem is referenced by:  relopab  5134  reli  5135  rele  5136  relcnv  5379  cotrg  5383  relco  5510  reloprab  6344  reldmoprab  6387  relrpss  6581  eqer  7363  ecopover  7434  relen  7541  reldom  7542  relfsupp  7851  relwdom  8013  fpwwe2lem2  9031  fpwwe2lem3  9032  fpwwe2lem6  9034  fpwwe2lem7  9035  fpwwe2lem9  9037  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwelem  9044  climrel  13315  rlimrel  13316  brstruct  14640  sscrel  15182  gaorber  16346  sylow2a  16639  efgrelexlemb  16768  efgcpbllemb  16773  rellindf  18843  tpsexOLD  19420  2ndcctbss  19956  refrel  20009  vitalilem1  22017  lgsquadlem1  23629  lgsquadlem2  23630  reluhgra  24294  relushgra  24295  relumgra  24314  reluslgra  24334  relusgra  24335  iscusgra0  24457  cusgrasize  24478  erclwwlkrel  24810  erclwwlknrel  24822  frisusgrapr  24991  relrngo  25379  drngoi  25409  isdivrngo  25433  vcrel  25440  h2hlm  25897  hlimi  26105  relmntop  28002  relae  28212  mptrel  29198  fnerel  30156  filnetlem3  30198  brabg2  30206  heiborlem3  30309  heiborlem4  30310  isdrngo1  30359  riscer  30391  prter1  30620  prter3  30623  reldvds  31220  relfusgra  32423  rellininds  33044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-xp 5010  df-rel 5011