Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ceqsexv GIF version

Theorem ceqsexv 2593
 Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
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 nfv 1421 . 2 𝑥𝜓
2 ceqsexv.1 . 2 𝐴 ∈ V
3 ceqsexv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsex 2592 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243  ∃wex 1381   ∈ wcel 1393  Vcvv 2557 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2559 This theorem is referenced by:  ceqsex3v  2596  gencbvex  2600  sbhypf  2603  euxfr2dc  2726  inuni  3909  eqvinop  3980  onm  4138  uniuni  4183  opeliunxp  4395  elvvv  4403  rexiunxp  4478  imai  4681  coi1  4836  abrexco  5398  opabex3d  5748  opabex3  5749  xpsnen  6295  xpcomco  6300  xpassen  6304
 Copyright terms: Public domain W3C validator