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

Theorem ceqsexv 2639
 Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
Hypotheses
Ref Expression
ceqsexv.1
ceqsexv.2
Assertion
Ref Expression
ceqsexv
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem ceqsexv
StepHypRef Expression
1 nfv 1462 . 2
2 ceqsexv.1 . 2
3 ceqsexv.2 . 2
41, 2, 3ceqsex 2638 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 102   wb 103   wceq 1285  wex 1422   wcel 1434  cvv 2602 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604 This theorem is referenced by:  ceqsex3v  2642  gencbvex  2646  sbhypf  2649  euxfr2dc  2778  inuni  3938  eqvinop  4006  onm  4164  uniuni  4209  opeliunxp  4421  elvvv  4429  rexiunxp  4506  imai  4711  coi1  4866  abrexco  5430  opabex3d  5779  opabex3  5780  xpsnen  6365  xpcomco  6370  xpassen  6374
 Copyright terms: Public domain W3C validator