MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbidv Structured version   Visualization version   Unicode version

Theorem exbidv 1776
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
albidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
exbidv  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem exbidv
StepHypRef Expression
1 ax-5 1766 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1735 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  2exbidv  1778  3exbidv  1779  eubid  2337  eleq1d  2533  eleq2dALT  2536  rexbidv2  2888  ceqsex2  3072  alexeqg  3156  sbc2or  3264  sbc5  3280  sbcex2  3306  sbcabel  3333  elpreqprlem  4152  elpreqpr  4153  eluni  4193  csbuni  4218  intab  4256  cbvopab1  4466  cbvopab1s  4468  axrep1  4509  axrep2  4510  axrep3  4511  zfrepclf  4514  axsep2  4519  zfauscl  4520  euotd  4702  opeliunxp  4891  brcog  5006  elrn2g  5030  dfdmf  5033  eldmg  5035  dfrnf  5079  elrn2  5080  elrnmpt1  5089  brcodir  5225  dfco2a  5342  cores  5345  sbcfung  5612  brprcneu  5872  ssimaexg  5946  dmfco  5954  fndmdif  6001  fmptco  6072  fliftf  6226  cbvoprab1  6382  cbvoprab2  6383  snnex  6616  uniuni  6619  dmtpos  7003  wrecseq123  7047  wfrlem1  7053  wfrlem3a  7056  wfrlem15  7068  rdglim2  7168  ecdmn0  7424  mapsn  7531  bren  7596  brdomg  7597  domeng  7601  isinf  7803  ac6sfi  7833  ordiso  8049  brwdom  8100  brwdom2  8106  zfregcl  8127  inf0  8144  zfinf  8162  bnd2  8382  isinffi  8444  acneq  8492  acni  8494  aceq0  8567  aceq3lem  8569  dfac3  8570  dfac5lem4  8575  dfac8  8583  dfac9  8584  kmlem1  8598  kmlem2  8599  kmlem8  8605  kmlem10  8607  kmlem13  8610  cfval  8695  cardcf  8700  cfeq0  8704  cfsuc  8705  cff1  8706  cflim3  8710  cofsmo  8717  isfin4  8745  axcc2lem  8884  axcc4dom  8889  domtriomlem  8890  dcomex  8895  axdc2lem  8896  axdc4lem  8903  zfac  8908  ac7g  8922  ac4c  8924  ac5  8925  ac6sg  8936  weth  8943  axrepndlem1  9035  axunndlem1  9038  zfcndrep  9057  zfcndinf  9061  zfcndac  9062  gruina  9261  grothomex  9272  genpass  9452  1idpr  9472  ltexprlem3  9481  ltexprlem4  9482  ltexpri  9486  reclem2pr  9491  reclem3pr  9492  recexpr  9494  infm3  10590  nnunb  10889  axdc4uz  12234  ishashinf  12667  relexpindlem  13203  sumeq1  13832  sumeq2w  13835  sumeq2ii  13836  summo  13860  fsum  13863  fsum2dlem  13908  ntrivcvgn0  14031  ntrivcvgmullem  14034  prodeq1f  14039  prodeq2w  14043  prodeq2ii  14044  prodmo  14067  zprod  14068  fprod  14072  fprodntriv  14073  fprod2dlem  14111  ncoprmgcdne1b  14734  vdwapun  15003  vdwmc  15007  vdwmc2  15008  isacs  15635  dfiso2  15755  brssc  15797  isssc  15803  equivestrcsetc  16115  dirge  16561  gsumvalx  16591  gsumpropd  16593  gsumpropd2lem  16594  gsumress  16597  gsumval3eu  17616  gsumval3lem2  17618  dprd2d2  17755  znleval  19202  neitr  20273  cmpcovf  20483  hausmapdom  20592  ptval  20662  elpt  20664  ptpjopn  20704  ptclsg  20707  ptcnp  20714  uffix2  21017  cnextf  21159  prdsxmslem2  21622  metustfbas  21650  metcld2  22354  dchrmusumlema  24410  dchrisum0lema  24431  istrkgld  24586  uvtx01vtx  25299  wlkiswwlk2  25504  wlklniswwlkn2  25507  wlknwwlknvbij  25547  clwlkisclwwlk  25596  clwwlkvbij  25608  isgrpo  26005  ismgmOLD  26129  adjeu  27623  fcoinvbr  28291  fmptcof2  28334  acunirnmpt  28336  acunirnmpt2  28337  acunirnmpt2f  28338  aciunf1  28340  fpwrelmapffslem  28392  fmcncfil  28811  bnj865  29806  bnj1388  29914  bnj1489  29937  eldm3  30473  opelco3  30491  frrlem1  30585  elsingles  30756  funpartlem  30780  dfrdg4  30789  linedegen  30981  finminlem  31045  filnetlem4  31108  bj-axrep1  31469  bj-axrep2  31470  bj-axrep3  31471  bj-eleq1w  31523  bj-eleq2w  31524  bj-issetwt  31536  bj-ax8  31563  bj-axsep2  31596  bj-finsumval0  31772  csbwrecsg  31798  csboprabg  31801  topdifinffinlem  31820  wl-sb8eut  31976  sdclem1  32136  fdc  32138  isriscg  32287  islshpat  32654  lshpsmreu  32746  isopos  32817  islpln5  33171  islvol5  33215  pmapjat1  33489  dibelval3  34786  diblsmopel  34810  mapdpglem3  35314  hdmapglem7a  35569  dfac11  35991  clcnvlem  36301  dfhe3  36441  iotasbc  36840  iotasbc2  36841  sbcexgOLD  36974  csbunigOLD  37275  csbxpgOLD  37277  csbrngOLD  37280  fnchoice  37413  mapsnd  37547  mapsnend  37551  stoweidlem35  38008  stoweidlem39  38012  uvtxa01vtx0  39633  1loopgrvd2  39725  opeliun2xp  40622
  Copyright terms: Public domain W3C validator