Theorem elopab 5511

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 3476	. 2 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2		opex 5445	. . . . 5 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
3		eleq1 2851	. . . . 5 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
4	2, 3	mpbiri 261	. . . 4 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
5	4	adantr 485	. . 3 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
6	5	exlimivv 1962	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7		elopabw 5510	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
8	1, 6, 7	pm5.21nii 381	1 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455  ⟨cop 4595  {copab 5173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3910  df-in 3912  df-ss 3922  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5174

This theorem is referenced by:  rexopabb  5512  vopelopabsb  5513  opelopabsb  5514  opelopabt  5516  opelopabga  5517  brab2d  5522  opabn0  5538  0nelopab  5550  elxp  5684  elopaba  5795  elcnv  5862  cnvopab  6137  dfmpt3  6669  fmptsng  7166  fmptsnd  7167  opabex3d  7958  opabex3rd  7959  opabex3  7960  fsplit  8108  rtrclreclem3  15093  isfunc  17916  griedg0ssusgr  29615  rgrusgrprc  29939  brabgaf  32951  qqhval2  34372  eulerpartlemgvv  34766  satfvsucsuc  35857  satf0op  35869  opelopabd  37785  opelopabb  37786  poimirlem26  38297  ecxrn  39055  dicelval3  41954  pellexlem5  43560  pellex  43562  opelopab4  45260  sprsymrelfvlem  48239  uspgrsprf  48911  uspgrsprf1  48912  brab2dd  49606