Theorem exbidv 1954

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  nfbidv  1955  2exbidv  1957  3exbidv  1958  eleq1w  2849  eleq2w  2850  eleq1d  2851  eleq2dALT  2853  clelab  2910  rexbidv2  3188  rmoeq1  3403  ceqsex2  3508  ceqsex2v  3509  alexeqg  3613  sbc2or  3756  sbc5ALT  3776  sbcex2  3807  sbcabel  3834  elpreqprlem  4836  elpreqpr  4837  eluni  4880  csbuni  4908  intab  4948  cbvopab1  5190  cbvopab1g  5191  cbvopab1s  5193  cbvopab1v  5194  axrep1  5244  axreplem  5245  zfrepclf  5257  axsepg  5263  sepg  5264  zfausclOLD  5266  sels  5426  euotd  5501  opeliunxp  5733  opeliun2xp  5734  brcog  5857  elrn2g  5885  dfdmf  5891  eldmg  5893  dmun  5905  dmopabelb  5911  dmopab2rex  5912  dm0rn0  5919  dfrnf  5945  elrnmpt1  5955  brcodir  6124  dfco2a  6252  cores  6255  sbcfung  6567  brprcneu  6878  brprcneuALT  6879  ssimaexg  6974  dmfco  6984  fndmdif  7044  fmptco  7132  fliftf  7324  imaeqsexvOLD  7374  oprabbidv  7489  cbvoprab1  7510  cbvoprab2  7511  cbvoprab12v  7513  imaeqexov  7661  uniuni  7770  dmtpos  8243  frecseq123  8288  csbfrecsg  8290  frrlem1  8292  frrlem13  8304  rdglim2  8428  ecdmn0  8756  mapsnd  8893  breng  8961  brdom2g  8963  domeng  8968  mapsnend  9043  isinf  9235  ac6sfi  9254  ordiso  9488  brwdom  9539  brwdom2  9545  zfregcl  9566  zfregclOLD  9567  inf0  9600  zfinf  9618  ttrcleq  9688  brttrcl  9692  brttrcl2  9693  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  bnd2  9895  isinffi  9997  acneq  10046  acni  10048  aceq0  10121  aceq3lem  10123  dfac3  10124  dfac5lem4  10129  dfac8  10138  dfac9  10139  kmlem1  10153  kmlem2  10154  kmlem8  10160  kmlem10  10162  kmlem13  10165  cfval  10248  cardcf  10253  cfeq0  10258  cfsuc  10259  cff1  10260  cflim3  10264  cofsmo  10271  isfin4  10299  axcc2lem  10438  axcc4dom  10443  domtriomlem  10444  dcomex  10449  axdc2lem  10450  axdc4lem  10457  zfac  10462  ac7g  10476  ac4c  10478  ac5  10479  ac6sg  10490  weth  10497  axrepndlem1  10595  axunndlem1  10598  zfcndrep  10617  zfcndinf  10621  zfcndac  10622  gruina  10821  grothomex  10832  genpass  11012  1idpr  11032  ltexprlem3  11041  ltexprlem4  11042  ltexpri  11046  reclem2pr  11051  reclem3pr  11052  recexpr  11054  infm3  12192  nnunb  12518  axdc4uz  14040  ishashinf  14520  relexpindlem  15126  sumeq1  15766  sumeq2w  15769  sumeq2ii  15770  sumeq2sdv  15780  summo  15794  fsum  15797  fsum2dlem  15847  ntrivcvgn0  15978  ntrivcvgmullem  15981  prodeq1f  15986  prodeq1  15987  prodeq2w  15990  prodeq2ii  15991  prodeq2sdv  16003  prodmo  16016  zprod  16017  fprod  16021  fprodntriv  16022  fprod2dlem  16060  vdwapun  17059  vdwmc  17063  vdwmc2  17064  isacs  17732  dfiso2  17854  brssc  17896  isssc  17902  equivestrcsetc  18233  dirge  18684  gsumvalx  18759  gsumpropd  18761  gsumpropd2lem  18762  gsumress  18765  gsumval3eu  19999  gsumval3lem2  20001  dprd2d2  20141  znleval  21734  neitr  23367  cmpcovf  23578  hausmapdom  23687  ptval  23757  elpt  23759  ptpjopn  23799  ptclsg  23802  ptcnp  23809  uffix2  24111  cnextf  24253  prdsxmslem2  24716  metustfbas  24744  metcld2  25496  dchrmusumlema  27687  dchrisum0lema  27708  elold  28082  lrrecfr  28166  istrkgld  28758  uvtx01vtx  29777  1loopgrvd2  29883  wspthsn  30227  iswspthn  30228  wspthsnon  30231  iswspthsnon  30235  wspthnon  30237  wlkiswwlks2  30254  wlkiswwlksupgr2  30256  wlklnwwlkln2lem  30261  wlksnwwlknvbij  30287  wspthsnwspthsnon  30295  elwwlks2on  30340  elwwlks2  30348  elwspths2spth  30349  clwlkclwwlk  30383  clwwlkvbij  30494  isgrpo  30879  adjeu  32271  iunrnmptss  32940  fcoinvbr  32980  2ndresdju  33024  fmptcof2  33032  acunirnmpt  33034  acunirnmpt2  33035  acunirnmpt2f  33036  aciunf1  33038  fnpreimac  33045  fpwrelmapffslem  33107  gsumwrd2dccatlem  33421  1arithidomlem1  33849  1arithidom  33851  fmcncfil  34345  bnj865  35335  bnj1388  35445  bnj1489  35468  fineqvrep  35543  fineqvac  35545  tz9.1regs  35563  satfrnmapom  35875  satf0op  35882  dmopab3rexdif  35910  prv1n  35936  rexxfr3dALT  36144  eldm3  36266  opelco3  36280  elsingles  36421  funpartlem  36447  dfrdg4  36456  linedegen  36648  prodeq12sdv  36763  cbvoprab2vw  36783  cbvoprab13vw  36786  cbvmodavw  36795  cbvopab1davw  36809  cbvopab2davw  36810  cbvoprab2davw  36817  cbvoprab12davw  36820  cbvoprab23davw  36821  cbvoprab13davw  36822  cbvsumdavw  36824  cbvproddavw  36825  cbvsumdavw2  36840  cbvproddavw2  36841  finminlem  36862  filnetlem4  36925  axtco1  37017  axtco1from2  37019  axtco1g  37020  dfttc4lem1  37072  dfttc4  37074  elttcirr  37075  ttcexg  37076  regsfromregtco  37082  mh-regprimbi  37089  mh-infprim1bi  37090  mobidvALT  37525  bj-issetwt  37543  bj-inex1gALT  37593  bj-axreprepsep  37745  bj-restuni  37772  bj-finsumval0  37962  csboprabg  38009  topdifinffinlem  38026  cbveud  38051  wl-sb8eut  38266  wl-sb8eutv  38267  sdclem1  38427  fdc  38429  ismgmOLD  38534  isriscg  38668  elrnres  38960  eldm4  38963  exan3  38982  exanres  38983  eldmcnv  39027  brxrn  39065  exeupre  39173  cosseq  39198  brcoss  39203  brcoss3  39205  eldm1cossres  39232  brcosscnv  39244  islshpat  39824  lshpsmreu  39916  isopos  39987  islpln5  40342  islvol5  40386  pmapjat1  40660  dibelval3  41954  diblsmopel  41978  mapdpglem3  42482  hdmapglem7a  42734  19.9dev  43019  fimgmcyc  43335  dfac11  43822  nnoeomeqom  44072  clcnvlem  44382  dfhe3  44534  ntrneineine0lem  44842  iotasbc  45162  iotasbc2  45163  brpermmodel  45745  permaxinf2lem  45754  permac8prim  45756  nregmodel  45759  fnchoice  45782  axccdom  45971  axccd  45977  stoweidlem35  46782  stoweidlem39  46786  dfatdmfcoafv2  48024  dfatco  48026  ichexmpl1  48251  ichnreuop  48254  ichreuopeq  48255  elsprel  48257  isgrim  48680  dfgric2  48713  gricushgr  48715  gricuspgr  48716  ushggricedg  48725  isubgrgrim  48727  uhgrimisgrgric  48729  grtri  48738  grtriprop  48739  isgrtri  48741  uspgrlim  48790  grlimedgclnbgr  48793  grlimgrtri  48801  dfgrlic2  48806  dfgrlic3  48808  grilcbri2  48809  map0cor  49666  nelsubc3lem  49881  thinccic  50282  istermc  50285  termcpropd  50314  discsntermlem  50381  basrestermcfolem  50382  discsnterm  50385  cnelsubclem  50414  bnd2d  50492