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

Theorem rexab 3690
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 3073 . . . 4 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥 ∈ {𝑦𝜑} ¬ 𝜒)
2 ralab.1 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
32ralab 3687 . . . 4 (∀𝑥 ∈ {𝑦𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒))
41, 3xchbinx 333 . . 3 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒))
5 imnang 1844 . . 3 (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓𝜒))
64, 5xchbinx 333 . 2 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓𝜒))
7 df-ex 1782 . 2 (∃𝑥(𝜓𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓𝜒))
86, 7bitr4i 277 1 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∃𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wal 1539  wex 1781  {cab 2709  wral 3061  wrex 3070
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 1913  ax-6 1971  ax-7 2011
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-ral 3062  df-rex 3071
This theorem is referenced by:  4sqlem12  16893  noinfno  27445  sleadd1  27699  addsuniflem  27711  addsasslem1  27713  addsasslem2  27714  mulsuniflem  27831  addsdilem1  27833  addsdilem2  27834  mulsasslem1  27845  mulsasslem2  27846  mblfinlem3  36830  mblfinlem4  36831  ismblfin  36832  itg2addnclem  36842  itg2addnc  36845  diophrex  41815
  Copyright terms: Public domain W3C validator