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

Theorem ceqsexv 3493
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2172. (Revised by Gino Giotto, 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 1846 . . 3 (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑))
2 ceqsexv.1 . . . 4 𝐴 ∈ V
3 ceqsexv.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
43notbid 318 . . . 4 (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
52, 4ceqsalv 3480 . . 3 (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓)
61, 5bitr3i 277 . 2 (¬ ∃𝑥(𝑥 = 𝐴𝜑) ↔ ¬ 𝜓)
76con4bii 321 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wex 1782  wcel 2107  Vcvv 3444
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
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811
This theorem is referenced by:  ceqsexv2d  3496  ceqsex2v  3498  ceqsex3v  3499  gencbvex  3503  euxfr2w  3679  euxfr2  3681  inuni  5301  eqvinop  5445  elvvv  5708  dmfco  6938  fndmdif  6993  fndmin  6996  fmptco  7076  abrexco  7192  imaeqsexv  7309  imaeqexov  7593  uniuni  7697  elxp4  7860  elxp5  7861  brtpos2  8164  xpsnen  9002  xpcomco  9009  xpassen  9013  brttrcl2  9655  dfac5lem2  10065  cf0  10192  ltexprlem4  10980  pceu  16723  4sqlem12  16833  vdwapun  16851  gsumval3eu  19686  dprd2d2  19828  znleval  20977  metrest  23896  sleadd1  27320  addsunif  27332  addsasslem1  27333  addsasslem2  27334  fmptcof2  31619  fpwrelmapffslem  31696  cusgredgex  33772  dfdm5  34403  dfrn5  34404  elima4  34406  brtxp  34511  brpprod  34516  elfix  34534  dfiota3  34554  brimg  34568  brapply  34569  brsuccf  34572  funpartlem  34573  brrestrict  34580  dfrecs2  34581  dfrdg4  34582  lshpsmreu  37617  isopos  37688  islpln5  38044  islvol5  38088  cdlemftr3  39074  dibelval3  39656  dicelval3  39689  mapdpglem3  40184  hdmapglem7a  40436  diophrex  41141
  Copyright terms: Public domain W3C validator