Theorem exbidv 1921

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

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  nfbidv  1922  2exbidv  1924  3exbidv  1925  eleq1w  2812  eleq2w  2813  eleq1d  2814  eleq2dALT  2816  clelab  2874  rexbidv2  3154  rmoeq1  3390  cgsex4gOLD  3498  ceqsex2  3504  ceqsex2v  3505  alexeqg  3620  sbc2or  3765  sbc5ALT  3785  sbcex2  3817  sbcabel  3844  elpreqprlem  4833  elpreqpr  4834  eluni  4877  csbuni  4903  intab  4945  cbvopab1  5184  cbvopab1g  5185  cbvopab1s  5187  cbvopab1v  5188  axrep1  5238  axreplem  5239  zfrepclf  5249  axsepg  5255  zfauscl  5256  sels  5401  euotd  5476  opeliunxp  5708  opeliun2xp  5709  brcog  5833  elrn2g  5857  dfdmf  5863  eldmg  5865  dmopabelb  5883  dmopab2rex  5884  dfrnf  5917  elrnmpt1  5927  brcodir  6095  dfco2a  6222  cores  6225  sbcfung  6543  brprcneu  6851  brprcneuALT  6852  ssimaexg  6950  dmfco  6960  fndmdif  7017  fmptco  7104  fliftf  7293  imaeqsexvOLD  7341  oprabbidv  7458  cbvoprab1  7479  cbvoprab2  7480  cbvoprab12v  7482  imaeqexov  7630  uniuni  7741  dmtpos  8220  frecseq123  8264  csbfrecsg  8266  frrlem1  8268  frrlem13  8280  rdglim2  8403  ecdmn0  8726  mapsnd  8862  breng  8930  brdom2g  8932  domeng  8937  mapsnend  9010  isinf  9214  isinfOLD  9215  ac6sfi  9238  ordiso  9476  brwdom  9527  brwdom2  9533  zfregcl  9554  inf0  9581  zfinf  9599  ttrcleq  9669  brttrcl  9673  brttrcl2  9674  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  bnd2  9853  isinffi  9952  acneq  10003  acni  10005  aceq0  10078  aceq3lem  10080  dfac3  10081  dfac5lem4  10086  dfac5lem4OLD  10088  dfac8  10096  dfac9  10097  kmlem1  10111  kmlem2  10112  kmlem8  10118  kmlem10  10120  kmlem13  10123  cfval  10207  cardcf  10212  cfeq0  10216  cfsuc  10217  cff1  10218  cflim3  10222  cofsmo  10229  isfin4  10257  axcc2lem  10396  axcc4dom  10401  domtriomlem  10402  dcomex  10407  axdc2lem  10408  axdc4lem  10415  zfac  10420  ac7g  10434  ac4c  10436  ac5  10437  ac6sg  10448  weth  10455  axrepndlem1  10552  axunndlem1  10555  zfcndrep  10574  zfcndinf  10578  zfcndac  10579  gruina  10778  grothomex  10789  genpass  10969  1idpr  10989  ltexprlem3  10998  ltexprlem4  10999  ltexpri  11003  reclem2pr  11008  reclem3pr  11009  recexpr  11011  infm3  12149  nnunb  12445  axdc4uz  13956  ishashinf  14435  relexpindlem  15036  sumeq1  15662  sumeq2w  15665  sumeq2ii  15666  sumeq2sdv  15676  summo  15690  fsum  15693  fsum2dlem  15743  ntrivcvgn0  15871  ntrivcvgmullem  15874  prodeq1f  15879  prodeq1  15880  prodeq2w  15883  prodeq2ii  15884  prodeq2sdv  15896  prodmo  15909  zprod  15910  fprod  15914  fprodntriv  15915  fprod2dlem  15953  vdwapun  16952  vdwmc  16956  vdwmc2  16957  isacs  17619  dfiso2  17741  brssc  17783  isssc  17789  equivestrcsetc  18120  dirge  18569  gsumvalx  18610  gsumpropd  18612  gsumpropd2lem  18613  gsumress  18616  gsumval3eu  19841  gsumval3lem2  19843  dprd2d2  19983  znleval  21471  neitr  23074  cmpcovf  23285  hausmapdom  23394  ptval  23464  elpt  23466  ptpjopn  23506  ptclsg  23509  ptcnp  23516  uffix2  23818  cnextf  23960  prdsxmslem2  24424  metustfbas  24452  metcld2  25214  dchrmusumlema  27411  dchrisum0lema  27432  elold  27788  lrrecfr  27857  istrkgld  28393  uvtx01vtx  29331  1loopgrvd2  29438  wspthsn  29785  iswspthn  29786  wspthsnon  29789  iswspthsnon  29793  wspthnon  29795  wlkiswwlks2  29812  wlkiswwlksupgr2  29814  wlklnwwlkln2lem  29819  wlksnwwlknvbij  29845  wspthsnwspthsnon  29853  elwwlks2on  29896  elwwlks2  29903  elwspths2spth  29904  clwlkclwwlk  29938  clwwlkvbij  30049  isgrpo  30433  adjeu  31825  iunrnmptss  32501  fcoinvbr  32541  2ndresdju  32580  fmptcof2  32588  acunirnmpt  32590  acunirnmpt2  32591  acunirnmpt2f  32592  aciunf1  32594  fnpreimac  32602  fpwrelmapffslem  32662  gsumwrd2dccatlem  33013  1arithidomlem1  33513  1arithidom  33515  fmcncfil  33928  bnj865  34920  bnj1388  35030  bnj1489  35053  fineqvrep  35092  fineqvac  35094  satfrnmapom  35364  satf0op  35371  dmopab3rexdif  35399  prv1n  35425  rexxfr3dALT  35633  eldm3  35755  opelco3  35769  elsingles  35913  funpartlem  35937  dfrdg4  35946  linedegen  36138  prodeq12sdv  36213  cbvoprab2vw  36233  cbvoprab13vw  36236  cbvmodavw  36245  cbvopab1davw  36259  cbvopab2davw  36260  cbvoprab2davw  36267  cbvoprab12davw  36270  cbvoprab23davw  36271  cbvoprab13davw  36272  cbvsumdavw  36274  cbvproddavw  36275  cbvsumdavw2  36290  cbvproddavw2  36291  finminlem  36313  filnetlem4  36376  mobidvALT  36852  bj-issetwt  36870  bj-restuni  37092  bj-finsumval0  37280  csboprabg  37325  topdifinffinlem  37342  cbveud  37367  wl-sb8eut  37573  wl-sb8eutv  37574  sdclem1  37744  fdc  37746  ismgmOLD  37851  isriscg  37985  elrnres  38267  eldm4  38270  exan3  38289  exanres  38290  eldmcnv  38334  brxrn  38363  cosseq  38424  brcoss  38429  brcoss3  38431  eldm1cossres  38458  brcosscnv  38470  islshpat  39017  lshpsmreu  39109  isopos  39180  islpln5  39536  islvol5  39580  pmapjat1  39854  dibelval3  41148  diblsmopel  41172  mapdpglem3  41676  hdmapglem7a  41928  19.9dev  42209  fimgmcyc  42529  dfac11  43058  nnoeomeqom  43308  clcnvlem  43619  dfhe3  43771  ntrneineine0lem  44079  iotasbc  44415  iotasbc2  44416  brpermmodel  45000  permaxinf2lem  45009  permac8prim  45011  nregmodel  45014  fnchoice  45030  axccdom  45223  axccd  45230  stoweidlem35  46040  stoweidlem39  46044  dfatdmfcoafv2  47259  dfatco  47261  ichexmpl1  47474  ichnreuop  47477  ichreuopeq  47478  elsprel  47480  isgrim  47886  dfgric2  47919  gricushgr  47921  gricuspgr  47922  ushggricedg  47931  isubgrgrim  47933  uhgrimisgrgric  47935  grtri  47943  grtriprop  47944  isgrtri  47946  uspgrlim  47995  grlimgrtri  47999  dfgrlic2  48004  dfgrlic3  48006  grilcbri2  48007  map0cor  48847  nelsubc3lem  49063  thinccic  49464  istermc  49467  termcpropd  49496  discsntermlem  49563  basrestermcfolem  49564  discsnterm  49567  cnelsubclem  49596  bnd2d  49674