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

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

Proof of Theorem elopab
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 elex 3510 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2 opex 5347 . . . . 5 𝑥, 𝑦⟩ ∈ V
3 eleq1 2897 . . . . 5 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
42, 3mpbiri 259 . . . 4 (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
54adantr 481 . . 3 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
65exlimivv 1924 . 2 (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7 eqeq1 2822 . . . . 5 (𝑧 = 𝐴 → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, 𝑦⟩))
87anbi1d 629 . . . 4 (𝑧 = 𝐴 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
982exbidv 1916 . . 3 (𝑧 = 𝐴 → (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
10 df-opab 5120 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
119, 10elab2g 3665 . 2 (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
121, 6, 11pm5.21nii 380 1 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1528  wex 1771  wcel 2105  Vcvv 3492  cop 4563  {copab 5119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5120
This theorem is referenced by:  rexopabb  5406  opelopabsbALT  5407  opelopabsb  5408  opelopabt  5410  opelopabga  5411  opabn0  5431  iunopab  5437  elopabr  5438  0nelopab  5443  epelgOLD  5460  elxp  5571  elopaelxp  5634  elopaba  5674  elcnv  5740  dfmpt3  6475  fmptsng  6922  fmptsnd  6923  opabex3d  7655  opabex3rd  7656  opabex3  7657  fsplit  7801  fsplitOLD  7802  rtrclreclem3  14407  isfunc  17122  griedg0ssusgr  26974  rgrusgrprc  27298  brabgaf  30287  qqhval2  31122  eulerpartlemgvv  31533  satfvsucsuc  32509  satf0op  32521  opelopabd  34325  opelopabb  34326  poimirlem26  34799  ecxrn  35519  dicelval3  38196  pellexlem5  39308  pellex  39310  opelopab4  40762  sprsymrelfvlem  43529  uspgrsprf  43898  uspgrsprf1  43899
  Copyright terms: Public domain W3C validator