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

Theorem ceqsexv 3532
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2177. (Revised by GG, 12-Oct-2024.) (Proof shortened by Wolf Lammen, 22-Jan-2025.)
Hypotheses
Ref Expression
ceqsexv.1 𝐴 ∈ V
ceqsexv.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ceqsexv (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ceqsexv
StepHypRef Expression
1 alinexa 1843 . . 3 (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑))
2 ceqsexv.1 . . . 4 𝐴 ∈ V
3 ceqsexv.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
43notbid 318 . . . 4 (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
52, 4ceqsalv 3521 . . 3 (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓)
61, 5bitr3i 277 . 2 (¬ ∃𝑥(𝑥 = 𝐴𝜑) ↔ ¬ 𝜓)
76con4bii 321 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1538   = wceq 1540  wex 1779  wcel 2108  Vcvv 3480
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  ax-8 2110
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816
This theorem is referenced by:  ceqsexv2dOLD  3534  ceqsex2v  3536  ceqsex3v  3537  gencbvex  3541  euxfr2w  3726  euxfr2  3728  inuni  5350  eqvinop  5492  elvvv  5761  dmfco  7005  fndmdif  7062  fndmin  7065  fmptco  7149  abrexco  7264  imaeqsexvOLD  7383  imaeqexov  7671  uniuni  7782  elxp4  7944  elxp5  7945  brtpos2  8257  xpsnen  9095  xpcomco  9102  xpassen  9106  brttrcl2  9754  dfac5lem2  10164  cf0  10291  ltexprlem4  11079  pceu  16884  4sqlem12  16994  vdwapun  17012  gsumval3eu  19922  dprd2d2  20064  znleval  21573  metrest  24537  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  mulsuniflem  28175  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  renegscl  28430  readdscl  28431  remulscl  28434  fmptcof2  32667  fpwrelmapffslem  32743  cusgredgex  35127  dfdm5  35773  dfrn5  35774  elima4  35776  brtxp  35881  brpprod  35886  elfix  35904  dfiota3  35924  brimg  35938  brapply  35939  brsuccf  35942  funpartlem  35943  brrestrict  35950  dfrecs2  35951  dfrdg4  35952  lshpsmreu  39110  isopos  39181  islpln5  39537  islvol5  39581  cdlemftr3  40567  dibelval3  41149  dicelval3  41182  mapdpglem3  41677  hdmapglem7a  41929  diophrex  42786
  Copyright terms: Public domain W3C validator