Theorem elopab 5526

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

Step	Hyp	Ref	Expression
1		elex 3491	. 2 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2		opex 5463	. . . . 5 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
3		eleq1 2819	. . . . 5 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
4	2, 3	mpbiri 257	. . . 4 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
5	4	adantr 479	. . 3 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
6	5	exlimivv 1933	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7		elopabw 5525	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
8	1, 6, 7	pm5.21nii 377	1 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1539  ∃wex 1779   ∈ wcel 2104  Vcvv 3472  ⟨cop 4633  {copab 5209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210

This theorem is referenced by:  rexopabb  5527  vopelopabsb  5528  opelopabsb  5529  opelopabt  5531  opelopabga  5532  opabn0  5552  iunopabOLD  5559  elopabrOLD  5562  0nelopab  5566  0nelopabOLD  5567  elxp  5698  elopaelxpOLD  5765  elopaba  5807  elcnv  5875  dfmpt3  6683  fmptsng  7167  fmptsnd  7168  opabex3d  7954  opabex3rd  7955  opabex3  7956  fsplit  8105  rtrclreclem3  15011  isfunc  17818  griedg0ssusgr  28789  rgrusgrprc  29113  brabgaf  32104  qqhval2  33260  eulerpartlemgvv  33673  satfvsucsuc  34654  satf0op  34666  opelopabd  36325  opelopabb  36326  poimirlem26  36817  ecxrn  37560  dicelval3  40354  pellexlem5  41873  pellex  41875  opelopab4  43614  sprsymrelfvlem  46456  uspgrsprf  46822  uspgrsprf1  46823