MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opabn0 Structured version   Visualization version   GIF version

Theorem opabn0 5152
Description: Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
opabn0 ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝑦𝜑)

Proof of Theorem opabn0
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 n0 4070 . 2 ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ≠ ∅ ↔ ∃𝑧 𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
2 elopab 5129 . . . 4 (𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
32exbii 1919 . . 3 (∃𝑧 𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑧𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
4 exrot3 2190 . . . 4 (∃𝑧𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5 opex 5077 . . . . . . 7 𝑥, 𝑦⟩ ∈ V
65isseti 3345 . . . . . 6 𝑧 𝑧 = ⟨𝑥, 𝑦
7 19.41v 2022 . . . . . 6 (∃𝑧(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (∃𝑧 𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
86, 7mpbiran 991 . . . . 5 (∃𝑧(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑)
982exbii 1920 . . . 4 (∃𝑥𝑦𝑧(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝜑)
104, 9bitri 264 . . 3 (∃𝑧𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝜑)
113, 10bitri 264 . 2 (∃𝑧 𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦𝜑)
121, 11bitri 264 1 ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝑦𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1628  wex 1849  wcel 2135  wne 2928  c0 4054  cop 4323  {copab 4860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pr 5051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-v 3338  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-opab 4861
This theorem is referenced by:  opab0  5153  csbopab  5154  dvdsrval  18841  thlle  20239  bcthlem5  23321  lgsquadlem3  25302  br1cosscnvxrn  34543
  Copyright terms: Public domain W3C validator