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

Theorem ceqsexv 2608
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 1435 . 2 𝑥𝜓
2 ceqsexv.1 . 2 𝐴 ∈ V
3 ceqsexv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsex 2607 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102   = wceq 1257  wex 1395  wcel 1407  Vcvv 2572
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-v 2574
This theorem is referenced by:  ceqsex3v  2611  gencbvex  2615  sbhypf  2618  euxfr2dc  2746  inuni  3934  eqvinop  4005  onm  4163  uniuni  4208  opeliunxp  4420  elvvv  4428  rexiunxp  4503  imai  4706  coi1  4861  abrexco  5423  opabex3d  5773  opabex3  5774  xpsnen  6323  xpcomco  6328  xpassen  6332
  Copyright terms: Public domain W3C validator