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

Theorem rexab 3691
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 3688 . . . 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  16889  noinfno  27221  sleadd1  27472  addsuniflem  27484  addsasslem1  27486  addsasslem2  27487  mulsuniflem  27604  addsdilem1  27606  addsdilem2  27607  mulsasslem1  27618  mulsasslem2  27619  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  itg2addnclem  36539  itg2addnc  36542  diophrex  41513
  Copyright terms: Public domain W3C validator