Theorem elopab 5475

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 3451	. 2 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2		opex 5411	. . . . 5 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
3		eleq1 2825	. . . . 5 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
4	2, 3	mpbiri 258	. . . 4 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
5	4	adantr 480	. . 3 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
6	5	exlimivv 1934	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7		elopabw 5474	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
8	1, 6, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430  ⟨cop 4574  {copab 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-in 3897  df-ss 3907  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149

This theorem is referenced by:  rexopabb  5476  vopelopabsb  5477  opelopabsb  5478  opelopabt  5480  opelopabga  5481  opabn0  5501  0nelopab  5513  elxp  5647  elopaba  5757  elcnv  5825  cnvopab  6094  dfmpt3  6626  fmptsng  7116  fmptsnd  7117  opabex3d  7911  opabex3rd  7912  opabex3  7913  fsplit  8060  rtrclreclem3  15013  isfunc  17822  griedg0ssusgr  29348  rgrusgrprc  29673  brab2d  32693  brabgaf  32694  qqhval2  34142  eulerpartlemgvv  34536  satfvsucsuc  35563  satf0op  35575  opelopabd  37471  opelopabb  37472  poimirlem26  37981  ecxrn  38741  dicelval3  41640  pellexlem5  43279  pellex  43281  opelopab4  44996  sprsymrelfvlem  47962  uspgrsprf  48634  uspgrsprf1  48635  brab2dd  49315