Theorem exbidv 1921

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1867 and exbid 2223. (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  2824  eleq2w  2825  eleq1d  2826  eleq2dALT  2828  clelab  2887  rexbidv2  3175  rmoeq1  3416  cgsex4gOLD  3529  ceqsex2  3535  ceqsex2v  3536  alexeqg  3651  sbc2or  3797  sbc5ALT  3817  sbcex2  3850  sbcabel  3878  elpreqprlem  4866  elpreqpr  4867  eluni  4910  csbuni  4936  intab  4978  cbvopab1  5217  cbvopab1g  5218  cbvopab1s  5220  cbvopab1v  5221  axrep1  5280  axreplem  5281  zfrepclf  5291  axsepg  5297  zfauscl  5298  sels  5443  euotd  5518  opeliunxp  5752  opeliun2xp  5753  brcog  5877  elrn2g  5901  dfdmf  5907  eldmg  5909  dmopabelb  5927  dmopab2rex  5928  dfrnf  5961  elrnmpt1  5971  brcodir  6139  dfco2a  6266  cores  6269  sbcfung  6590  brprcneu  6896  brprcneuALT  6897  ssimaexg  6995  dmfco  7005  fndmdif  7062  fmptco  7149  fliftf  7335  imaeqsexvOLD  7383  oprabbidv  7499  cbvoprab1  7520  cbvoprab2  7521  cbvoprab12v  7523  imaeqexov  7671  uniuni  7782  dmtpos  8263  frecseq123  8307  csbfrecsg  8309  frrlem1  8311  frrlem13  8323  wrecseq123OLD  8340  wfrlem1OLD  8348  wfrlem3OLDa  8351  wfrlem15OLD  8363  rdglim2  8472  ecdmn0  8794  mapsnd  8926  breng  8994  brdom2g  8996  brdomgOLD  8998  domeng  9003  mapsnend  9076  isinf  9296  isinfOLD  9297  ac6sfi  9320  ordiso  9556  brwdom  9607  brwdom2  9613  zfregcl  9634  inf0  9661  zfinf  9679  ttrcleq  9749  brttrcl  9753  brttrcl2  9754  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  bnd2  9933  isinffi  10032  acneq  10083  acni  10085  aceq0  10158  aceq3lem  10160  dfac3  10161  dfac5lem4  10166  dfac5lem4OLD  10168  dfac8  10176  dfac9  10177  kmlem1  10191  kmlem2  10192  kmlem8  10198  kmlem10  10200  kmlem13  10203  cfval  10287  cardcf  10292  cfeq0  10296  cfsuc  10297  cff1  10298  cflim3  10302  cofsmo  10309  isfin4  10337  axcc2lem  10476  axcc4dom  10481  domtriomlem  10482  dcomex  10487  axdc2lem  10488  axdc4lem  10495  zfac  10500  ac7g  10514  ac4c  10516  ac5  10517  ac6sg  10528  weth  10535  axrepndlem1  10632  axunndlem1  10635  zfcndrep  10654  zfcndinf  10658  zfcndac  10659  gruina  10858  grothomex  10869  genpass  11049  1idpr  11069  ltexprlem3  11078  ltexprlem4  11079  ltexpri  11083  reclem2pr  11088  reclem3pr  11089  recexpr  11091  infm3  12227  nnunb  12522  axdc4uz  14025  ishashinf  14502  relexpindlem  15102  sumeq1  15725  sumeq2w  15728  sumeq2ii  15729  sumeq2sdv  15739  summo  15753  fsum  15756  fsum2dlem  15806  ntrivcvgn0  15934  ntrivcvgmullem  15937  prodeq1f  15942  prodeq1  15943  prodeq2w  15946  prodeq2ii  15947  prodeq2sdv  15959  prodmo  15972  zprod  15973  fprod  15977  fprodntriv  15978  fprod2dlem  16016  vdwapun  17012  vdwmc  17016  vdwmc2  17017  isacs  17694  dfiso2  17816  brssc  17858  isssc  17864  equivestrcsetc  18197  dirge  18648  gsumvalx  18689  gsumpropd  18691  gsumpropd2lem  18692  gsumress  18695  gsumval3eu  19922  gsumval3lem2  19924  dprd2d2  20064  znleval  21573  neitr  23188  cmpcovf  23399  hausmapdom  23508  ptval  23578  elpt  23580  ptpjopn  23620  ptclsg  23623  ptcnp  23630  uffix2  23932  cnextf  24074  prdsxmslem2  24542  metustfbas  24570  metcld2  25341  dchrmusumlema  27537  dchrisum0lema  27558  elold  27908  lrrecfr  27976  istrkgld  28467  uvtx01vtx  29414  1loopgrvd2  29521  wspthsn  29868  iswspthn  29869  wspthsnon  29872  iswspthsnon  29876  wspthnon  29878  wlkiswwlks2  29895  wlkiswwlksupgr2  29897  wlklnwwlkln2lem  29902  wlksnwwlknvbij  29928  wspthsnwspthsnon  29936  elwwlks2on  29979  elwwlks2  29986  elwspths2spth  29987  clwlkclwwlk  30021  clwwlkvbij  30132  isgrpo  30516  adjeu  31908  iunrnmptss  32578  fcoinvbr  32618  2ndresdju  32659  fmptcof2  32667  acunirnmpt  32669  acunirnmpt2  32670  acunirnmpt2f  32671  aciunf1  32673  fnpreimac  32681  fpwrelmapffslem  32743  gsumwrd2dccatlem  33069  1arithidomlem1  33563  1arithidom  33565  fmcncfil  33930  bnj865  34937  bnj1388  35047  bnj1489  35070  fineqvrep  35109  fineqvac  35111  satfrnmapom  35375  satf0op  35382  dmopab3rexdif  35410  prv1n  35436  rexxfr3dALT  35644  eldm3  35761  opelco3  35775  elsingles  35919  funpartlem  35943  dfrdg4  35952  linedegen  36144  prodeq12sdv  36219  cbvoprab2vw  36239  cbvoprab13vw  36242  cbvmodavw  36251  cbvopab1davw  36265  cbvopab2davw  36266  cbvoprab2davw  36273  cbvoprab12davw  36276  cbvoprab23davw  36277  cbvoprab13davw  36278  cbvsumdavw  36280  cbvproddavw  36281  cbvsumdavw2  36296  cbvproddavw2  36297  finminlem  36319  filnetlem4  36382  mobidvALT  36858  bj-issetwt  36876  bj-restuni  37098  bj-finsumval0  37286  csboprabg  37331  topdifinffinlem  37348  cbveud  37373  wl-sb8eut  37579  wl-sb8eutv  37580  sdclem1  37750  fdc  37752  ismgmOLD  37857  isriscg  37991  elrnres  38272  eldm4  38275  exan3  38295  exanres  38296  eldmcnv  38346  brxrn  38375  cosseq  38427  brcoss  38432  brcoss3  38434  eldm1cossres  38461  brcosscnv  38473  islshpat  39018  lshpsmreu  39110  isopos  39181  islpln5  39537  islvol5  39581  pmapjat1  39855  dibelval3  41149  diblsmopel  41173  mapdpglem3  41677  hdmapglem7a  41929  19.9dev  42253  fimgmcyc  42544  dfac11  43074  nnoeomeqom  43325  clcnvlem  43636  dfhe3  43788  ntrneineine0lem  44096  iotasbc  44438  iotasbc2  44439  fnchoice  45034  axccdom  45227  axccd  45234  stoweidlem35  46050  stoweidlem39  46054  dfatdmfcoafv2  47266  dfatco  47268  ichexmpl1  47456  ichnreuop  47459  ichreuopeq  47460  elsprel  47462  isgrim  47868  dfgric2  47884  gricushgr  47886  gricuspgr  47887  ushggricedg  47896  isubgrgrim  47897  uhgrimisgrgric  47899  grtri  47907  grtriprop  47908  isgrtri  47910  uspgrlim  47959  grlimgrtri  47963  dfgrlic2  47968  dfgrlic3  47970  grilcbri2  47971  map0cor  48764  thinccic  49118  istermc  49121  termcpropd  49135  bnd2d  49200