MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  relopabi Structured version   Visualization version   GIF version

Theorem relopabi 5156
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 Rel 𝐴

Proof of Theorem relopabi
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 relopabi.1 . . . 4 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2 df-opab 4638 . . . 4 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
31, 2eqtri 2631 . . 3 𝐴 = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
4 vex 3175 . . . . . . . 8 𝑥 ∈ V
5 vex 3175 . . . . . . . 8 𝑦 ∈ V
64, 5opelvv 5078 . . . . . . 7 𝑥, 𝑦⟩ ∈ (V × V)
7 eleq1 2675 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ (V × V) ↔ ⟨𝑥, 𝑦⟩ ∈ (V × V)))
86, 7mpbiri 246 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 ∈ (V × V))
98adantr 479 . . . . 5 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝑧 ∈ (V × V))
109exlimivv 1846 . . . 4 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝑧 ∈ (V × V))
1110abssi 3639 . . 3 {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} ⊆ (V × V)
123, 11eqsstri 3597 . 2 𝐴 ⊆ (V × V)
13 df-rel 5035 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
1412, 13mpbir 219 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wex 1694  wcel 1976  {cab 2595  Vcvv 3172  wss 3539  cop 4130  {copab 4636   × cxp 5026  Rel wrel 5033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-opab 4638  df-xp 5034  df-rel 5035
This theorem is referenced by:  relopab  5157  mptrel  5158  reli  5159  rele  5160  relcnv  5409  cotrg  5413  relco  5536  reloprab  6578  reldmoprab  6621  relrpss  6813  eqer  7641  eqerOLD  7642  ecopover  7715  ecopoverOLD  7716  relen  7823  reldom  7824  relfsupp  8137  relwdom  8331  fpwwe2lem2  9310  fpwwe2lem3  9311  fpwwe2lem6  9313  fpwwe2lem7  9314  fpwwe2lem9  9316  fpwwe2lem11  9318  fpwwe2lem12  9319  fpwwe2lem13  9320  fpwwelem  9323  climrel  14017  rlimrel  14018  brstruct  15649  sscrel  16242  gaorber  17510  sylow2a  17803  efgrelexlemb  17932  efgcpbllemb  17937  rellindf  19908  2ndcctbss  21010  refrel  21063  vitalilem1  23099  vitalilem1OLD  23100  lgsquadlem1  24822  lgsquadlem2  24823  reluhgra  25589  relushgra  25590  relumgra  25609  reluslgra  25629  relusgra  25630  iscusgra0  25752  cusgrasize  25772  erclwwlkrel  26104  erclwwlknrel  26116  frisusgrapr  26284  vcrel  26568  h2hlm  27027  hlimi  27235  relmntop  29202  relae  29436  fnerel  31309  filnetlem3  31351  brabg2  32483  heiborlem3  32585  heiborlem4  32586  relrngo  32668  isdivrngo  32722  drngoi  32723  isdrngo1  32728  riscer  32760  prter1  32985  prter3  32988  reldvds  37339  relsubgr  40495  erclwwlksrel  41240  erclwwlksnrel  41252  rellininds  42028
  Copyright terms: Public domain W3C validator