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

Theorem rexab 3689
Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro, 3-Sep-2015.) Reduce axiom usage. (Revised by Gino Giotto, 2-Nov-2024.)
Hypothesis
Ref Expression
ralab.1 (𝑦 = 𝑥 → (𝜑𝜓))
Assertion
Ref Expression
rexab (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∃𝑥(𝜓𝜒))
Distinct variable groups:   𝑥,𝑦   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑥,𝑦)

Proof of Theorem rexab
StepHypRef Expression
1 dfrex2 3074 . . . 4 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥 ∈ {𝑦𝜑} ¬ 𝜒)
2 ralab.1 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
32ralab 3686 . . . 4 (∀𝑥 ∈ {𝑦𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒))
41, 3xchbinx 334 . . 3 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒))
5 imnang 1845 . . 3 (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓𝜒))
64, 5xchbinx 334 . 2 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓𝜒))
7 df-ex 1783 . 2 (∃𝑥(𝜓𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓𝜒))
86, 7bitr4i 278 1 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∃𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540  wex 1782  {cab 2710  wral 3062  wrex 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-ral 3063  df-rex 3072
This theorem is referenced by:  4sqlem12  16885  noinfno  27201  sleadd1  27452  addsuniflem  27464  addsasslem1  27466  addsasslem2  27467  mulsuniflem  27584  addsdilem1  27586  addsdilem2  27587  mulsasslem1  27598  mulsasslem2  27599  mblfinlem3  36465  mblfinlem4  36466  ismblfin  36467  itg2addnclem  36477  itg2addnc  36480  diophrex  41446
  Copyright terms: Public domain W3C validator