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

Theorem rexsng 4679
Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 30-Sep-2024.)
Hypothesis
Ref Expression
ralsng.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rexsng (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem rexsng
StepHypRef Expression
1 ralsng.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
21notbid 318 . . 3 (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
32ralsng 4678 . 2 (𝐴𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓))
4 dfrex2 3074 . . 3 (∃𝑥 ∈ {𝐴}𝜑 ↔ ¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑)
5 bicom1 220 . . . 4 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜓 ↔ ∀𝑥 ∈ {𝐴} ¬ 𝜑))
65con1bid 356 . . 3 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑𝜓))
74, 6bitrid 283 . 2 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (∃𝑥 ∈ {𝐴}𝜑𝜓))
83, 7syl 17 1 (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1542  wcel 2107  wral 3062  wrex 3071  {csn 4629
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  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-sn 4630
This theorem is referenced by:  rexsn  4687  rextpg  4704  iunxsng  5094  frirr  5654  frsn  5764  imasng  6083  naddunif  8692  scshwfzeqfzo  14777  dvdsprmpweqnn  16818  mnd1  18667  grp1  18930  elntg2  28274  1loopgrvd0  28792  1egrvtxdg0  28799  nfrgr2v  29556  1vwmgr  29560  elgrplsmsn  32531  grplsmid  32545  ballotlemfc0  33522  ballotlemfcc  33523  bj-restsn  36011  elrnressn  37189  elpaddat  38723  elpadd2at  38725  brfvidRP  42487  mnuunid  43084  iccelpart  46149  pzriprnglem3  46855  pzriprnglem10  46862  zlidlring  46874  lco0  47156
  Copyright terms: Public domain W3C validator