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

Theorem rexab 3700
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 GG, 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 3697 . . . 4 (∀𝑥 ∈ {𝑦𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒))
41, 3xchbinx 334 . . 3 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒))
5 imnang 1842 . . 3 (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓𝜒))
64, 5xchbinx 334 . 2 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓𝜒))
7 df-ex 1780 . 2 (∃𝑥(𝜓𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓𝜒))
86, 7bitr4i 278 1 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∃𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1538  wex 1779  {cab 2714  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-ral 3062  df-rex 3071
This theorem is referenced by:  4sqlem12  16994  noinfno  27763  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  mulsuniflem  28175  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  renegscl  28430  readdscl  28431  remulscl  28434  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  itg2addnc  37681  diophrex  42786
  Copyright terms: Public domain W3C validator