NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ceqsexv GIF version

Theorem ceqsexv 2894
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
Hypotheses
Ref Expression
ceqsexv.1 A V
ceqsexv.2 (x = A → (φψ))
Assertion
Ref Expression
ceqsexv (x(x = A φ) ↔ ψ)
Distinct variable groups:   x,A   ψ,x
Allowed substitution hint:   φ(x)

Proof of Theorem ceqsexv
StepHypRef Expression
1 nfv 1619 . 2 xψ
2 ceqsexv.1 . 2 A V
3 ceqsexv.2 . 2 (x = A → (φψ))
41, 2, 3ceqsex 2893 1 (x(x = A φ) ↔ ψ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358  wex 1541   = wceq 1642   wcel 1710  Vcvv 2859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861
This theorem is referenced by:  ceqsex3v  2897  gencbvex  2901  sbhypf  2904  euxfr2  3021  elpw12  4145  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  eluni1g  4172  opkelcokg  4261  opkelimagekg  4271  dfimak2  4298  insklem  4304  ndisjrelk  4323  unipw1  4325  dfpw2  4327  dfaddc2  4381  dfnnc2  4395  elsuc  4413  addcass  4415  nnsucelrlem1  4424  ltfinex  4464  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspsslem1  4550  vfinspss  4551  vfinncsp  4554  dfop2lem1  4573  eqvinop  4606  el1st  4729  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem6  4736  setconslem7  4737  df1st2  4738  dfswap2  4741  dfid3  4768  opeliunxp  4820  elimapw1  4944  elimapw12  4945  elimapw13  4946  elimapw11c  4948  imai  5010  dmsnopg  5066  rnsnop  5075  coi1  5094  dfcnv2  5100  elxp4  5108  df2nd2  5111  iunfopab  5204  dmfco  5381  abrexco  5463  isomin  5496  opbr1st  5501  opbr2nd  5502  dfoprab2  5558  brsnsi1  5775  brsnsi2  5776  brco1st  5777  brco2nd  5778  trtxp  5781  elfix  5787  brimage  5793  oqelins4  5794  txpcofun  5803  otsnelsi3  5805  addcfnex  5824  funsex  5828  qrpprod  5836  pw1fnf1o  5855  clos1ex  5876  enex  6031  xpassenlem  6056  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  enpw1pw  6075  enprmaplem1  6076  ovmuc  6130  mucex  6133  ovcelem1  6171  ceexlem1  6173  ceex  6174  el2c  6191  taddc  6229  tcfnex  6244  csucex  6259  nnltp1clem1  6261  addccan2nclem1  6263  addccan2nclem2  6264  nmembers1lem1  6268  nncdiv3lem1  6275  nncdiv3lem2  6276  nnc3n3p1  6278  spacvallem1  6281  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304
  Copyright terms: Public domain W3C validator