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

Theorem exbidv 1922
Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1868 and exbid 2224. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
albidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
exbidv (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem exbidv
StepHypRef Expression
1 ax-5 1911 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2exbidh 1868 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  nfbidv  1923  2exbidv  1925  3exbidv  1926  eleq1w  2875  eleq2w  2876  eleq1d  2877  eleq2dALT  2879  nfcriOLD  2949  rexbidv2  3257  cgsex4g  3489  ceqsex2  3494  ceqsex2v  3495  alexeqg  3595  sbc2or  3732  sbc5  3751  sbcex2  3784  sbcabel  3810  elpreqprlem  4759  elpreqpr  4760  eluni  4806  csbuni  4832  intab  4871  cbvopab1  5106  cbvopab1g  5107  cbvopab1s  5109  axrep1  5158  axreplem  5159  zfrepclf  5165  axsepg  5171  zfauscl  5172  euotd  5371  opeliunxp  5587  brcog  5705  elrn2g  5729  dfdmf  5733  eldmg  5735  dmopabelb  5753  dmopab2rex  5754  dfrnf  5788  elrn2  5789  elrnmpt1  5798  brcodir  5950  dfco2a  6070  cores  6073  sbcfung  6352  brprcneu  6641  ssimaexg  6728  dmfco  6738  fndmdif  6793  fmptco  6872  fliftf  7051  cbvoprab1  7224  cbvoprab2  7225  uniuni  7468  dmtpos  7891  wrecseq123  7935  wfrlem1  7941  wfrlem3a  7944  wfrlem15  7956  rdglim2  8055  ecdmn0  8323  mapsnd  8437  bren  8505  brdomg  8506  domeng  8510  mapsnend  8575  isinf  8719  ac6sfi  8750  ordiso  8968  brwdom  9019  brwdom2  9025  zfregcl  9046  inf0  9072  zfinf  9090  bnd2  9310  isinffi  9409  acneq  9458  acni  9460  aceq0  9533  aceq3lem  9535  dfac3  9536  dfac5lem4  9541  dfac8  9550  dfac9  9551  kmlem1  9565  kmlem2  9566  kmlem8  9572  kmlem10  9574  kmlem13  9577  cfval  9662  cardcf  9667  cfeq0  9671  cfsuc  9672  cff1  9673  cflim3  9677  cofsmo  9684  isfin4  9712  axcc2lem  9851  axcc4dom  9856  domtriomlem  9857  dcomex  9862  axdc2lem  9863  axdc4lem  9870  zfac  9875  ac7g  9889  ac4c  9891  ac5  9892  ac6sg  9903  weth  9910  axrepndlem1  10007  axunndlem1  10010  zfcndrep  10029  zfcndinf  10033  zfcndac  10034  gruina  10233  grothomex  10244  genpass  10424  1idpr  10444  ltexprlem3  10453  ltexprlem4  10454  ltexpri  10458  reclem2pr  10463  reclem3pr  10464  recexpr  10466  infm3  11591  nnunb  11885  axdc4uz  13351  ishashinf  13821  relexpindlem  14417  sumeq1  15040  sumeq2w  15044  sumeq2ii  15045  summo  15069  fsum  15072  fsum2dlem  15120  ntrivcvgn0  15249  ntrivcvgmullem  15252  prodeq1f  15257  prodeq2w  15261  prodeq2ii  15262  prodmo  15285  zprod  15286  fprod  15290  fprodntriv  15291  fprod2dlem  15329  vdwapun  16303  vdwmc  16307  vdwmc2  16308  isacs  16917  dfiso2  17037  brssc  17079  isssc  17085  equivestrcsetc  17397  dirge  17842  gsumvalx  17881  gsumpropd  17883  gsumpropd2lem  17884  gsumress  17887  gsumval3eu  19020  gsumval3lem2  19022  dprd2d2  19162  znleval  20249  neitr  21788  cmpcovf  21999  hausmapdom  22108  ptval  22178  elpt  22180  ptpjopn  22220  ptclsg  22223  ptcnp  22230  uffix2  22532  cnextf  22674  prdsxmslem2  23139  metustfbas  23167  metcld2  23914  dchrmusumlema  26080  dchrisum0lema  26101  istrkgld  26256  uvtx01vtx  27190  1loopgrvd2  27296  wspthsn  27637  iswspthn  27638  wspthsnon  27641  iswspthsnon  27645  wspthnon  27647  wlkiswwlks2  27664  wlkiswwlksupgr2  27666  wlklnwwlkln2lem  27671  wlksnwwlknvbij  27697  wspthsnwspthsnon  27705  elwwlks2on  27748  elwwlks2  27755  elwspths2spth  27756  clwlkclwwlk  27790  clwwlkvbij  27901  isgrpo  28283  adjeu  29675  iunrnmptss  30332  fcoinvbr  30374  2ndresdju  30414  fmptcof2  30423  acunirnmpt  30425  acunirnmpt2  30426  acunirnmpt2f  30427  aciunf1  30429  fnpreimac  30437  fpwrelmapffslem  30497  fmcncfil  31282  bnj865  32303  bnj1388  32413  bnj1489  32436  satfrnmapom  32725  satf0op  32732  dmopab3rexdif  32760  prv1n  32786  eldm3  33105  opelco3  33126  frecseq123  33227  frrlem1  33231  frrlem13  33243  elsingles  33487  funpartlem  33511  dfrdg4  33520  linedegen  33712  finminlem  33774  filnetlem4  33837  mobidvALT  34291  bj-issetwt  34308  bj-restuni  34507  bj-finsumval0  34695  csbwrecsg  34739  csboprabg  34742  topdifinffinlem  34759  cbveud  34784  wl-sb8eut  34971  wl-dfrmof  35013  sdclem1  35174  fdc  35176  ismgmOLD  35281  isriscg  35415  eldm4  35684  exan3  35704  exanres  35705  eldmcnv  35755  brxrn  35779  cosseq  35824  brcoss  35829  brcoss3  35831  eldm1cossres  35853  brcosscnv  35865  islshpat  36306  lshpsmreu  36398  isopos  36469  islpln5  36824  islvol5  36868  pmapjat1  37142  dibelval3  38436  diblsmopel  38460  mapdpglem3  38964  hdmapglem7a  39216  19.9dev  39383  dfac11  39993  clcnvlem  40310  dfhe3  40463  ntrneineine0lem  40773  iotasbc  41110  iotasbc2  41111  fnchoice  41645  axccdom  41840  axccd  41848  stoweidlem35  42664  stoweidlem39  42668  dfatdmfcoafv2  43797  dfatco  43799  ichexmpl1  43973  ichnreuop  43976  ichreuopeq  43977  elsprel  43979  isomgr  44328  isomgreqve  44330  isomushgr  44331  isomuspgr  44339  isomgrsym  44341  isomgrtr  44344  ushrisomgr  44346  opeliun2xp  44721  bnd2d  45198
  Copyright terms: Public domain W3C validator