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

Theorem elopab 5441
Description: Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998.)
Assertion
Ref Expression
elopab (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem elopab
StepHypRef Expression
1 elex 3451 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2 opex 5380 . . . . 5 𝑥, 𝑦⟩ ∈ V
3 eleq1 2827 . . . . 5 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
42, 3mpbiri 257 . . . 4 (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
54adantr 481 . . 3 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
65exlimivv 1936 . 2 (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7 elopabw 5440 . 2 (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
81, 6, 7pm5.21nii 380 1 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1539  wex 1782  wcel 2107  Vcvv 3433  cop 4568  {copab 5137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5138
This theorem is referenced by:  rexopabb  5442  vopelopabsb  5443  opelopabsb  5444  opelopabt  5446  opelopabga  5447  opabn0  5467  iunopabOLD  5474  elopabrOLD  5477  0nelopab  5481  0nelopabOLD  5482  elxp  5613  elopaelxpOLD  5678  elopaba  5720  elcnv  5788  dfmpt3  6576  fmptsng  7049  fmptsnd  7050  opabex3d  7817  opabex3rd  7818  opabex3  7819  fsplit  7966  fsplitOLD  7967  rtrclreclem3  14780  isfunc  17588  griedg0ssusgr  27641  rgrusgrprc  27965  brabgaf  30957  qqhval2  31941  eulerpartlemgvv  32352  satfvsucsuc  33336  satf0op  33348  opelopabd  35321  opelopabb  35322  poimirlem26  35812  ecxrn  36524  dicelval3  39201  pellexlem5  40662  pellex  40664  opelopab4  42178  sprsymrelfvlem  44953  uspgrsprf  45319  uspgrsprf1  45320
  Copyright terms: Public domain W3C validator