Theorem elopab 5536

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477  ⟨cop 4636  {copab 5209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5210

This theorem is referenced by:  rexopabb  5537  vopelopabsb  5538  opelopabsb  5539  opelopabt  5541  opelopabga  5542  opabn0  5562  iunopabOLD  5569  elopabrOLD  5572  0nelopab  5576  elxp  5711  elopaelxpOLD  5778  elopaba  5820  elcnv  5889  cnvopab  6159  dfmpt3  6702  fmptsng  7187  fmptsnd  7188  opabex3d  7988  opabex3rd  7989  opabex3  7990  fsplit  8140  rtrclreclem3  15095  isfunc  17914  griedg0ssusgr  29296  rgrusgrprc  29621  brab2d  32626  brabgaf  32627  qqhval2  33944  eulerpartlemgvv  34357  satfvsucsuc  35349  satf0op  35361  opelopabd  37123  opelopabb  37124  poimirlem26  37632  ecxrn  38368  dicelval3  41162  pellexlem5  42820  pellex  42822  opelopab4  44548  sprsymrelfvlem  47414  uspgrsprf  47989  uspgrsprf1  47990