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

Theorem ceqsexv2d 3533
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025.) (Proof shortened by SN, 5-Jun-2025.)
Hypotheses
Ref Expression
ceqsexv2d.1 𝐴 ∈ V
ceqsexv2d.2 (𝑥 = 𝐴 → (𝜑𝜓))
ceqsexv2d.3 𝜓
Assertion
Ref Expression
ceqsexv2d 𝑥𝜑
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem ceqsexv2d
StepHypRef Expression
1 ceqsexv2d.1 . . 3 𝐴 ∈ V
21isseti 3498 . 2 𝑥 𝑥 = 𝐴
3 ceqsexv2d.3 . . 3 𝜓
4 ceqsexv2d.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
53, 4mpbiri 258 . 2 (𝑥 = 𝐴𝜑)
62, 5eximii 1837 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = 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:  en0  9058  en0r  9060  ensn1  9061  0domg  9140  tz9.1  9769  cplem2  9930  karden  9935  pwmnd  18950  2lgslem1  27438  griedg0prc  29281  1loopgrvd2  29521  bnj150  34890  fnchoice  45034  nfermltl8rev  47729  nfermltl2rev  47730  nfermltlrev  47731  nn0mnd  48095  rrx2xpreen  48640
  Copyright terms: Public domain W3C validator