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

Theorem ceqsexv 2725
 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 1508 . 2
2 ceqsexv.1 . 2
3 ceqsexv.2 . 2
41, 2, 3ceqsex 2724 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wceq 1331  wex 1468   wcel 1480  cvv 2686 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688 This theorem is referenced by:  ceqsex3v  2728  gencbvex  2732  sbhypf  2735  euxfr2dc  2869  inuni  4080  eqvinop  4165  onm  4323  uniuni  4372  opeliunxp  4594  elvvv  4602  rexiunxp  4681  imai  4895  coi1  5054  abrexco  5660  opabex3d  6019  opabex3  6020  mapsnen  6705  xpsnen  6715  xpcomco  6720  xpassen  6724
 Copyright terms: Public domain W3C validator