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 3496 . 2 𝑥 𝑥 = 𝐴
3 ceqsexv2d.3 . . 3 𝜓
4 ceqsexv2d.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
53, 4mpbiri 258 . 2 (𝑥 = 𝐴𝜑)
62, 5eximii 1834 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1537  wex 1776  wcel 2106  Vcvv 3478
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  ax-8 2108
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814
This theorem is referenced by:  en0  9057  en0r  9059  ensn1  9060  0domg  9139  tz9.1  9767  cplem2  9928  karden  9933  pwmnd  18963  2lgslem1  27453  griedg0prc  29296  1loopgrvd2  29536  bnj150  34869  fnchoice  44967  nfermltl8rev  47667  nfermltl2rev  47668  nfermltlrev  47669  nn0mnd  48023  rrx2xpreen  48569
  Copyright terms: Public domain W3C validator