Theorem elopab 5513

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 3478	. 2 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2		opex 5447	. . . . 5 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
3		eleq1 2853	. . . . 5 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
4	2, 3	mpbiri 261	. . . 4 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
5	4	adantr 486	. . 3 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
6	5	exlimivv 1965	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7		elopabw 5512	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
8	1, 6, 7	pm5.21nii 381	1 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3457  ⟨cop 4597  {copab 5175

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-un 3911  df-in 3913  df-ss 3923  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5176

This theorem is used by:  rexopabb  5514  vopelopabsb  5515  opelopabsb  5516  opelopabt  5518  opelopabga  5519  brab2d  5524  opabn0  5540  0nelopab  5552  elxp  5686  elopaba  5797  elcnv  5864  cnvopab  6139  dfmpt3  6673  fmptsng  7172  fmptsnd  7173  opabex3d  7968  opabex3rd  7969  opabex3  7970  fsplit  8118  rtrclreclem3  15121  isfunc  17943  griedg0ssusgr  29673  rgrusgrprc  29997  brabgaf  33022  qqhval2  34436  eulerpartlemgvv  34831  satfvsucsuc  35894  satf0op  35906  opelopabd  37842  opelopabb  37843  poimirlem26  38354  ecxrn  39113  dicelval3  42012  pellexlem5  43618  pellex  43620  opelopab4  45318  sprsymrelfvlem  48297  uspgrsprf  48969  uspgrsprf1  48970  brab2dd  49663