Theorem exbidv 1922

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1868 and exbid 2226. (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

Step	Hyp	Ref	Expression
1		ax-5 1911	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1868	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  nfbidv  1923  2exbidv  1925  3exbidv  1926  eleq1w  2814  eleq2w  2815  eleq1d  2816  eleq2dALT  2818  clelab  2876  rexbidv2  3152  rmoeq1  3377  cgsex4gOLD  3484  ceqsex2  3489  ceqsex2v  3490  alexeqg  3601  sbc2or  3745  sbc5ALT  3765  sbcex2  3797  sbcabel  3824  elpreqprlem  4815  elpreqpr  4816  eluni  4859  csbuni  4886  intab  4926  cbvopab1  5163  cbvopab1g  5164  cbvopab1s  5166  cbvopab1v  5167  axrep1  5216  axreplem  5217  zfrepclf  5227  axsepg  5233  zfauscl  5234  sels  5379  euotd  5451  opeliunxp  5681  opeliun2xp  5682  brcog  5805  elrn2g  5829  dfdmf  5835  eldmg  5837  dmopabelb  5855  dmopab2rex  5856  dm0rn0  5863  dfrnf  5889  elrnmpt1  5899  brcodir  6065  dfco2a  6193  cores  6196  sbcfung  6505  brprcneu  6812  brprcneuALT  6813  ssimaexg  6908  dmfco  6918  fndmdif  6975  fmptco  7062  fliftf  7249  imaeqsexvOLD  7297  oprabbidv  7412  cbvoprab1  7433  cbvoprab2  7434  cbvoprab12v  7436  imaeqexov  7584  uniuni  7695  dmtpos  8168  frecseq123  8212  csbfrecsg  8214  frrlem1  8216  frrlem13  8228  rdglim2  8351  ecdmn0  8674  mapsnd  8810  breng  8878  brdom2g  8880  domeng  8885  mapsnend  8958  isinf  9149  ac6sfi  9168  ordiso  9402  brwdom  9453  brwdom2  9459  zfregcl  9480  zfregclOLD  9481  inf0  9511  zfinf  9529  ttrcleq  9599  brttrcl  9603  brttrcl2  9604  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  ttrclselem2  9616  bnd2  9786  isinffi  9885  acneq  9934  acni  9936  aceq0  10009  aceq3lem  10011  dfac3  10012  dfac5lem4  10017  dfac5lem4OLD  10019  dfac8  10027  dfac9  10028  kmlem1  10042  kmlem2  10043  kmlem8  10049  kmlem10  10051  kmlem13  10054  cfval  10138  cardcf  10143  cfeq0  10147  cfsuc  10148  cff1  10149  cflim3  10153  cofsmo  10160  isfin4  10188  axcc2lem  10327  axcc4dom  10332  domtriomlem  10333  dcomex  10338  axdc2lem  10339  axdc4lem  10346  zfac  10351  ac7g  10365  ac4c  10367  ac5  10368  ac6sg  10379  weth  10386  axrepndlem1  10483  axunndlem1  10486  zfcndrep  10505  zfcndinf  10509  zfcndac  10510  gruina  10709  grothomex  10720  genpass  10900  1idpr  10920  ltexprlem3  10929  ltexprlem4  10930  ltexpri  10934  reclem2pr  10939  reclem3pr  10940  recexpr  10942  infm3  12081  nnunb  12377  axdc4uz  13891  ishashinf  14370  relexpindlem  14970  sumeq1  15596  sumeq2w  15599  sumeq2ii  15600  sumeq2sdv  15610  summo  15624  fsum  15627  fsum2dlem  15677  ntrivcvgn0  15805  ntrivcvgmullem  15808  prodeq1f  15813  prodeq1  15814  prodeq2w  15817  prodeq2ii  15818  prodeq2sdv  15830  prodmo  15843  zprod  15844  fprod  15848  fprodntriv  15849  fprod2dlem  15887  vdwapun  16886  vdwmc  16890  vdwmc2  16891  isacs  17557  dfiso2  17679  brssc  17721  isssc  17727  equivestrcsetc  18058  dirge  18509  gsumvalx  18584  gsumpropd  18586  gsumpropd2lem  18587  gsumress  18590  gsumval3eu  19816  gsumval3lem2  19818  dprd2d2  19958  znleval  21491  neitr  23095  cmpcovf  23306  hausmapdom  23415  ptval  23485  elpt  23487  ptpjopn  23527  ptclsg  23530  ptcnp  23537  uffix2  23839  cnextf  23981  prdsxmslem2  24444  metustfbas  24472  metcld2  25234  dchrmusumlema  27431  dchrisum0lema  27452  elold  27814  lrrecfr  27886  istrkgld  28437  uvtx01vtx  29375  1loopgrvd2  29482  wspthsn  29826  iswspthn  29827  wspthsnon  29830  iswspthsnon  29834  wspthnon  29836  wlkiswwlks2  29853  wlkiswwlksupgr2  29855  wlklnwwlkln2lem  29860  wlksnwwlknvbij  29886  wspthsnwspthsnon  29894  elwwlks2on  29939  elwwlks2  29947  elwspths2spth  29948  clwlkclwwlk  29982  clwwlkvbij  30093  isgrpo  30477  adjeu  31869  iunrnmptss  32545  fcoinvbr  32585  2ndresdju  32631  fmptcof2  32639  acunirnmpt  32641  acunirnmpt2  32642  acunirnmpt2f  32643  aciunf1  32645  fnpreimac  32653  fpwrelmapffslem  32715  gsumwrd2dccatlem  33046  1arithidomlem1  33500  1arithidom  33502  fmcncfil  33944  bnj865  34935  bnj1388  35045  bnj1489  35068  tz9.1regs  35130  fineqvrep  35137  fineqvac  35139  satfrnmapom  35414  satf0op  35421  dmopab3rexdif  35449  prv1n  35475  rexxfr3dALT  35683  eldm3  35805  opelco3  35819  elsingles  35960  funpartlem  35986  dfrdg4  35995  linedegen  36187  prodeq12sdv  36262  cbvoprab2vw  36282  cbvoprab13vw  36285  cbvmodavw  36294  cbvopab1davw  36308  cbvopab2davw  36309  cbvoprab2davw  36316  cbvoprab12davw  36319  cbvoprab23davw  36320  cbvoprab13davw  36321  cbvsumdavw  36323  cbvproddavw  36324  cbvsumdavw2  36339  cbvproddavw2  36340  finminlem  36362  filnetlem4  36425  mobidvALT  36901  bj-issetwt  36919  bj-restuni  37141  bj-finsumval0  37329  csboprabg  37374  topdifinffinlem  37391  cbveud  37416  wl-sb8eut  37622  wl-sb8eutv  37623  sdclem1  37793  fdc  37795  ismgmOLD  37900  isriscg  38034  elrnres  38320  eldm4  38323  exan3  38342  exanres  38343  eldmcnv  38387  brxrn  38417  exeupre  38513  cosseq  38538  brcoss  38543  brcoss3  38545  eldm1cossres  38572  brcosscnv  38584  islshpat  39126  lshpsmreu  39218  isopos  39289  islpln5  39644  islvol5  39688  pmapjat1  39962  dibelval3  41256  diblsmopel  41280  mapdpglem3  41784  hdmapglem7a  42036  19.9dev  42317  fimgmcyc  42637  dfac11  43165  nnoeomeqom  43415  clcnvlem  43726  dfhe3  43878  ntrneineine0lem  44186  iotasbc  44522  iotasbc2  44523  brpermmodel  45106  permaxinf2lem  45115  permac8prim  45117  nregmodel  45120  fnchoice  45136  axccdom  45329  axccd  45336  stoweidlem35  46143  stoweidlem39  46147  dfatdmfcoafv2  47364  dfatco  47366  ichexmpl1  47579  ichnreuop  47582  ichreuopeq  47583  elsprel  47585  isgrim  47992  dfgric2  48025  gricushgr  48027  gricuspgr  48028  ushggricedg  48037  isubgrgrim  48039  uhgrimisgrgric  48041  grtri  48050  grtriprop  48051  isgrtri  48053  uspgrlim  48102  grlimedgclnbgr  48105  grlimgrtri  48113  dfgrlic2  48118  dfgrlic3  48120  grilcbri2  48121  map0cor  48965  nelsubc3lem  49181  thinccic  49582  istermc  49585  termcpropd  49614  discsntermlem  49681  basrestermcfolem  49682  discsnterm  49685  cnelsubclem  49714  bnd2d  49792