Theorem exbidv 1923

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1869 and exbid 2231. (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 1912	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1869	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∃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 1912

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

This theorem is referenced by:  nfbidv  1924  2exbidv  1926  3exbidv  1927  eleq1w  2819  eleq2w  2820  eleq1d  2821  eleq2dALT  2823  clelab  2880  rexbidv2  3157  rmoeq1  3373  ceqsex2  3481  ceqsex2v  3482  alexeqg  3593  sbc2or  3737  sbc5ALT  3757  sbcex2  3789  sbcabel  3816  elpreqprlem  4809  elpreqpr  4810  eluni  4853  csbuni  4880  intab  4920  cbvopab1  5159  cbvopab1g  5160  cbvopab1s  5162  cbvopab1v  5163  axrep1  5213  axreplem  5214  zfrepclf  5226  axsepg  5232  zfauscl  5233  sels  5392  euotd  5467  opeliunxp  5698  opeliun2xp  5699  brcog  5821  elrn2g  5845  dfdmf  5851  eldmg  5853  dmun  5865  dmopabelb  5871  dmopab2rex  5872  dm0rn0  5879  dfrnf  5905  elrnmpt1  5915  brcodir  6082  dfco2a  6210  cores  6213  sbcfung  6522  brprcneu  6830  brprcneuALT  6831  ssimaexg  6926  dmfco  6936  fndmdif  6994  fmptco  7082  fliftf  7270  imaeqsexvOLD  7318  oprabbidv  7433  cbvoprab1  7454  cbvoprab2  7455  cbvoprab12v  7457  imaeqexov  7605  uniuni  7716  dmtpos  8188  frecseq123  8232  csbfrecsg  8234  frrlem1  8236  frrlem13  8248  rdglim2  8371  ecdmn0  8696  mapsnd  8834  breng  8902  brdom2g  8904  domeng  8909  mapsnend  8983  isinf  9175  ac6sfi  9194  ordiso  9431  brwdom  9482  brwdom2  9488  zfregcl  9509  zfregclOLD  9510  inf0  9542  zfinf  9560  ttrcleq  9630  brttrcl  9634  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  bnd2  9817  isinffi  9916  acneq  9965  acni  9967  aceq0  10040  aceq3lem  10042  dfac3  10043  dfac5lem4  10048  dfac5lem4OLD  10050  dfac8  10058  dfac9  10059  kmlem1  10073  kmlem2  10074  kmlem8  10080  kmlem10  10082  kmlem13  10085  cfval  10169  cardcf  10174  cfeq0  10178  cfsuc  10179  cff1  10180  cflim3  10184  cofsmo  10191  isfin4  10219  axcc2lem  10358  axcc4dom  10363  domtriomlem  10364  dcomex  10369  axdc2lem  10370  axdc4lem  10377  zfac  10382  ac7g  10396  ac4c  10398  ac5  10399  ac6sg  10410  weth  10417  axrepndlem1  10515  axunndlem1  10518  zfcndrep  10537  zfcndinf  10541  zfcndac  10542  gruina  10741  grothomex  10752  genpass  10932  1idpr  10952  ltexprlem3  10961  ltexprlem4  10962  ltexpri  10966  reclem2pr  10971  reclem3pr  10972  recexpr  10974  infm3  12115  nnunb  12433  axdc4uz  13946  ishashinf  14425  relexpindlem  15025  sumeq1  15651  sumeq2w  15654  sumeq2ii  15655  sumeq2sdv  15665  summo  15679  fsum  15682  fsum2dlem  15732  ntrivcvgn0  15863  ntrivcvgmullem  15866  prodeq1f  15871  prodeq1  15872  prodeq2w  15875  prodeq2ii  15876  prodeq2sdv  15888  prodmo  15901  zprod  15902  fprod  15906  fprodntriv  15907  fprod2dlem  15945  vdwapun  16945  vdwmc  16949  vdwmc2  16950  isacs  17617  dfiso2  17739  brssc  17781  isssc  17787  equivestrcsetc  18118  dirge  18569  gsumvalx  18644  gsumpropd  18646  gsumpropd2lem  18647  gsumress  18650  gsumval3eu  19879  gsumval3lem2  19881  dprd2d2  20021  znleval  21534  neitr  23145  cmpcovf  23356  hausmapdom  23465  ptval  23535  elpt  23537  ptpjopn  23577  ptclsg  23580  ptcnp  23587  uffix2  23889  cnextf  24031  prdsxmslem2  24494  metustfbas  24522  metcld2  25274  dchrmusumlema  27456  dchrisum0lema  27477  elold  27851  lrrecfr  27935  istrkgld  28527  uvtx01vtx  29466  1loopgrvd2  29572  wspthsn  29916  iswspthn  29917  wspthsnon  29920  iswspthsnon  29924  wspthnon  29926  wlkiswwlks2  29943  wlkiswwlksupgr2  29945  wlklnwwlkln2lem  29950  wlksnwwlknvbij  29976  wspthsnwspthsnon  29984  elwwlks2on  30029  elwwlks2  30037  elwspths2spth  30038  clwlkclwwlk  30072  clwwlkvbij  30183  isgrpo  30568  adjeu  31960  iunrnmptss  32635  fcoinvbr  32675  2ndresdju  32722  fmptcof2  32730  acunirnmpt  32732  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1  32736  fnpreimac  32743  fpwrelmapffslem  32805  gsumwrd2dccatlem  33138  1arithidomlem1  33595  1arithidom  33597  fmcncfil  34075  bnj865  35065  bnj1388  35175  bnj1489  35198  fineqvrep  35258  fineqvac  35260  tz9.1regs  35278  satfrnmapom  35552  satf0op  35559  dmopab3rexdif  35587  prv1n  35613  rexxfr3dALT  35821  eldm3  35943  opelco3  35957  elsingles  36098  funpartlem  36124  dfrdg4  36133  linedegen  36325  prodeq12sdv  36400  cbvoprab2vw  36420  cbvoprab13vw  36423  cbvmodavw  36432  cbvopab1davw  36446  cbvopab2davw  36447  cbvoprab2davw  36454  cbvoprab12davw  36457  cbvoprab23davw  36458  cbvoprab13davw  36459  cbvsumdavw  36461  cbvproddavw  36462  cbvsumdavw2  36477  cbvproddavw2  36478  finminlem  36500  filnetlem4  36563  axtco1  36655  axtco1from2  36657  axtco1g  36658  dfttc4lem1  36710  dfttc4  36712  elttcirr  36713  ttcexg  36714  regsfromregtco  36720  mh-regprimbi  36727  mh-infprim1bi  36728  mobidvALT  37164  bj-issetwt  37182  bj-axreprepsep  37382  bj-restuni  37409  bj-finsumval0  37599  csboprabg  37646  topdifinffinlem  37663  cbveud  37688  wl-sb8eut  37903  wl-sb8eutv  37904  sdclem1  38064  fdc  38066  ismgmOLD  38171  isriscg  38305  elrnres  38599  eldm4  38602  exan3  38621  exanres  38622  eldmcnv  38666  brxrn  38704  exeupre  38812  cosseq  38837  brcoss  38842  brcoss3  38844  eldm1cossres  38871  brcosscnv  38883  islshpat  39463  lshpsmreu  39555  isopos  39626  islpln5  39981  islvol5  40025  pmapjat1  40299  dibelval3  41593  diblsmopel  41617  mapdpglem3  42121  hdmapglem7a  42373  19.9dev  42656  fimgmcyc  42979  dfac11  43490  nnoeomeqom  43740  clcnvlem  44050  dfhe3  44202  ntrneineine0lem  44510  iotasbc  44846  iotasbc2  44847  brpermmodel  45430  permaxinf2lem  45439  permac8prim  45441  nregmodel  45444  fnchoice  45460  axccdom  45651  axccd  45658  stoweidlem35  46463  stoweidlem39  46467  dfatdmfcoafv2  47702  dfatco  47704  ichexmpl1  47929  ichnreuop  47932  ichreuopeq  47933  elsprel  47935  isgrim  48358  dfgric2  48391  gricushgr  48393  gricuspgr  48394  ushggricedg  48403  isubgrgrim  48405  uhgrimisgrgric  48407  grtri  48416  grtriprop  48417  isgrtri  48419  uspgrlim  48468  grlimedgclnbgr  48471  grlimgrtri  48479  dfgrlic2  48484  dfgrlic3  48486  grilcbri2  48487  map0cor  49330  nelsubc3lem  49545  thinccic  49946  istermc  49949  termcpropd  49978  discsntermlem  50045  basrestermcfolem  50046  discsnterm  50049  cnelsubclem  50078  bnd2d  50156