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

Theorem elopab 5012
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 3243 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2 opex 4962 . . . . 5 𝑥, 𝑦⟩ ∈ V
3 eleq1 2718 . . . . 5 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
42, 3mpbiri 248 . . . 4 (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
54adantr 480 . . 3 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
65exlimivv 1900 . 2 (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7 eqeq1 2655 . . . . 5 (𝑧 = 𝐴 → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, 𝑦⟩))
87anbi1d 741 . . . 4 (𝑧 = 𝐴 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
982exbidv 1892 . . 3 (𝑧 = 𝐴 → (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
10 df-opab 4746 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
119, 10elab2g 3385 . 2 (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
121, 6, 11pm5.21nii 367 1 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231  cop 4216  {copab 4745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-opab 4746
This theorem is referenced by:  opelopabsbALT  5013  opelopabsb  5014  opelopabt  5016  opelopabga  5017  opabn0  5035  iunopab  5041  elopabr  5042  epelg  5059  elxp  5165  elopaelxp  5225  elopaba  5265  elcnv  5331  dfmpt3  6052  fmptsng  6475  fmptsnd  6476  0neqopab  6740  opabex3d  7187  opabex3  7188  fsplit  7327  rtrclreclem3  13844  isfunc  16571  griedg0ssusgr  26202  rgrusgrprc  26541  brabgaf  29546  qqhval2  30154  eulerpartlemgvv  30566  poimirlem26  33565  ecxrn  34289  dicelval3  36786  pellexlem5  37714  pellex  37716  opelopab4  39084  sprsymrelfvlem  42065  uspgrsprf  42079  uspgrsprf1  42080
  Copyright terms: Public domain W3C validator