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

Theorem rexab 3703
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 3071 . . . 4 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥 ∈ {𝑦𝜑} ¬ 𝜒)
2 ralab.1 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
32ralab 3700 . . . 4 (∀𝑥 ∈ {𝑦𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒))
41, 3xchbinx 334 . . 3 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒))
5 imnang 1839 . . 3 (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓𝜒))
64, 5xchbinx 334 . 2 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓𝜒))
7 df-ex 1777 . 2 (∃𝑥(𝜓𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓𝜒))
86, 7bitr4i 278 1 (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∃𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1535  wex 1776  {cab 2712  wral 3059  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-ral 3060  df-rex 3069
This theorem is referenced by:  4sqlem12  16990  noinfno  27778  sleadd1  28037  addsuniflem  28049  addsasslem1  28051  addsasslem2  28052  mulsuniflem  28190  addsdilem1  28192  addsdilem2  28193  mulsasslem1  28204  mulsasslem2  28205  renegscl  28445  readdscl  28446  remulscl  28449  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  itg2addnclem  37658  itg2addnc  37661  diophrex  42763
  Copyright terms: Public domain W3C validator