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

Theorem elopab 5385
 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
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3429 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2 opex 5325 . . . . 5 𝑥, 𝑦⟩ ∈ V
3 eleq1 2840 . . . . 5 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
42, 3mpbiri 261 . . . 4 (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
54adantr 485 . . 3 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
65exlimivv 1934 . 2 (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7 eqeq1 2763 . . . . 5 (𝑧 = 𝑤 → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝑤 = ⟨𝑥, 𝑦⟩))
87anbi1d 633 . . . 4 (𝑧 = 𝑤 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
982exbidv 1926 . . 3 (𝑧 = 𝑤 → (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
10 eqeq1 2763 . . . . 5 (𝑤 = 𝐴 → (𝑤 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, 𝑦⟩))
1110anbi1d 633 . . . 4 (𝑤 = 𝐴 → ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
12112exbidv 1926 . . 3 (𝑤 = 𝐴 → (∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
13 df-opab 5096 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
149, 12, 13elab2gw 3587 . 2 (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
151, 6, 14pm5.21nii 384 1 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  Vcvv 3410  ⟨cop 4529  {copab 5095 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-dif 3862  df-un 3864  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-opab 5096 This theorem is referenced by:  rexopabb  5386  vopelopabsb  5387  opelopabsb  5388  opelopabt  5390  opelopabga  5391  opabn0  5411  iunopab  5417  elopabr  5418  0nelopab  5423  elxp  5548  elopaelxp  5611  elopaba  5651  elcnv  5717  dfmpt3  6466  fmptsng  6922  fmptsnd  6923  opabex3d  7671  opabex3rd  7672  opabex3  7673  fsplit  7818  fsplitOLD  7819  rtrclreclem3  14468  isfunc  17194  griedg0ssusgr  27155  rgrusgrprc  27479  brabgaf  30471  qqhval2  31452  eulerpartlemgvv  31863  satfvsucsuc  32844  satf0op  32856  opelopabd  34837  opelopabb  34838  poimirlem26  35364  ecxrn  36080  dicelval3  38757  pellexlem5  40148  pellex  40150  opelopab4  41631  sprsymrelfvlem  44376  uspgrsprf  44742  uspgrsprf1  44743
 Copyright terms: Public domain W3C validator