Theorem elopab 5304

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.

Step	Hyp	Ref	Expression
1		elex 3455	. 2 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝐴 ∈ V)
2		opex 5248	. . . . 5 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
3		eleq1 2870	. . . . 5 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ V ↔ ⟨𝑥, 𝑦⟩ ∈ V))
4	2, 3	mpbiri 259	. . . 4 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝐴 ∈ V)
5	4	adantr 481	. . 3 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
6	5	exlimivv 1910	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝐴 ∈ V)
7		eqeq1 2799	. . . . 5 ⊢ (𝑧 = 𝐴 → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, 𝑦⟩))
8	7	anbi1d 629	. . . 4 ⊢ (𝑧 = 𝐴 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
9	8	2exbidv 1902	. . 3 ⊢ (𝑧 = 𝐴 → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
10		df-opab 5025	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
11	9, 10	elab2g 3607	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
12	1, 6, 11	pm5.21nii 380	1 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1522  ∃wex 1761   ∈ wcel 2081  Vcvv 3437  ⟨cop 4478  {copab 5024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-opab 5025

This theorem is referenced by:  rexopabb  5305  opelopabsbALT  5306  opelopabsb  5307  opelopabt  5309  opelopabga  5310  opabn0  5328  iunopab  5334  elopabr  5335  0nelopab  5340  epelgOLD  5355  elxp  5466  elopaelxp  5527  elopaba  5567  elcnv  5633  dfmpt3  6350  fmptsng  6793  fmptsnd  6794  opabex3d  7522  opabex3rd  7523  opabex3  7524  fsplit  7668  rtrclreclem3  14253  isfunc  16963  griedg0ssusgr  26730  rgrusgrprc  27054  brabgaf  30049  qqhval2  30840  eulerpartlemgvv  31251  satfvsucsuc  32221  satf0op  32233  poimirlem26  34468  ecxrn  35189  dicelval3  37866  pellexlem5  38934  pellex  38936  opelopab4  40443  sprsymrelfvlem  43154  uspgrsprf  43523  uspgrsprf1  43524