Theorem exbidv 1948

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

Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  nfbidv  1949  2exbidv  1951  3exbidv  1952  eleq1w  2852  eleq2w  2853  eleq1d  2854  eleq2dALT  2856  clelab  2913  rexbidv2  3191  rmoeq1  3407  ceqsex2  3513  ceqsex2v  3514  alexeqg  3619  sbc2or  3762  sbc5ALT  3782  sbcex2  3813  sbcabel  3840  elpreqprlem  4835  elpreqpr  4836  eluni  4879  csbuni  4907  intab  4947  cbvopab1  5189  cbvopab1g  5190  cbvopab1s  5192  cbvopab1v  5193  axrep1  5243  axreplem  5244  zfrepclf  5256  axsepg  5262  zfauscl  5263  sels  5422  euotd  5497  opeliunxp  5729  opeliun2xp  5730  brcog  5853  elrn2g  5881  dfdmf  5887  eldmg  5889  dmun  5901  dmopabelb  5907  dmopab2rex  5908  dm0rn0  5915  dfrnf  5941  elrnmpt1  5951  brcodir  6120  dfco2a  6248  cores  6251  sbcfung  6561  brprcneu  6872  brprcneuALT  6873  ssimaexg  6968  dmfco  6978  fndmdif  7038  fmptco  7126  fliftf  7314  imaeqsexvOLD  7362  oprabbidv  7477  cbvoprab1  7498  cbvoprab2  7499  cbvoprab12v  7501  imaeqexov  7649  uniuni  7761  dmtpos  8234  frecseq123  8279  csbfrecsg  8281  frrlem1  8283  frrlem13  8295  rdglim2  8419  ecdmn0  8747  mapsnd  8884  breng  8952  brdom2g  8954  domeng  8959  mapsnend  9033  isinf  9225  ac6sfi  9244  ordiso  9478  brwdom  9529  brwdom2  9535  zfregcl  9556  zfregclOLD  9557  inf0  9590  zfinf  9608  ttrcleq  9678  brttrcl  9682  brttrcl2  9683  ssttrcl  9684  ttrcltr  9685  ttrclss  9689  ttrclselem2  9695  bnd2  9879  isinffi  9978  acneq  10027  acni  10029  aceq0  10102  aceq3lem  10104  dfac3  10105  dfac5lem4  10110  dfac8  10119  dfac9  10120  kmlem1  10134  kmlem2  10135  kmlem8  10141  kmlem10  10143  kmlem13  10146  cfval  10230  cardcf  10235  cfeq0  10240  cfsuc  10241  cff1  10242  cflim3  10246  cofsmo  10253  isfin4  10281  axcc2lem  10420  axcc4dom  10425  domtriomlem  10426  dcomex  10431  axdc2lem  10432  axdc4lem  10439  zfac  10444  ac7g  10458  ac4c  10460  ac5  10461  ac6sg  10472  weth  10479  axrepndlem1  10577  axunndlem1  10580  zfcndrep  10599  zfcndinf  10603  zfcndac  10604  gruina  10803  grothomex  10814  genpass  10994  1idpr  11014  ltexprlem3  11023  ltexprlem4  11024  ltexpri  11028  reclem2pr  11033  reclem3pr  11034  recexpr  11036  infm3  12174  nnunb  12500  axdc4uz  14020  ishashinf  14500  relexpindlem  15100  sumeq1  15740  sumeq2w  15743  sumeq2ii  15744  sumeq2sdv  15754  summo  15768  fsum  15771  fsum2dlem  15821  ntrivcvgn0  15952  ntrivcvgmullem  15955  prodeq1f  15960  prodeq1  15961  prodeq2w  15964  prodeq2ii  15965  prodeq2sdv  15977  prodmo  15990  zprod  15991  fprod  15995  fprodntriv  15996  fprod2dlem  16034  vdwapun  17034  vdwmc  17038  vdwmc2  17039  isacs  17707  dfiso2  17829  brssc  17871  isssc  17877  equivestrcsetc  18208  dirge  18659  gsumvalx  18734  gsumpropd  18736  gsumpropd2lem  18737  gsumress  18740  gsumval3eu  19974  gsumval3lem2  19976  dprd2d2  20116  znleval  21673  neitr  23306  cmpcovf  23517  hausmapdom  23626  ptval  23696  elpt  23698  ptpjopn  23738  ptclsg  23741  ptcnp  23748  uffix2  24050  cnextf  24192  prdsxmslem2  24655  metustfbas  24683  metcld2  25435  dchrmusumlema  27623  dchrisum0lema  27644  elold  28018  lrrecfr  28102  istrkgld  28694  uvtx01vtx  29688  1loopgrvd2  29794  wspthsn  30138  iswspthn  30139  wspthsnon  30142  iswspthsnon  30146  wspthnon  30148  wlkiswwlks2  30165  wlkiswwlksupgr2  30167  wlklnwwlkln2lem  30172  wlksnwwlknvbij  30198  wspthsnwspthsnon  30206  elwwlks2on  30251  elwwlks2  30259  elwspths2spth  30260  clwlkclwwlk  30294  clwwlkvbij  30405  isgrpo  30790  adjeu  32182  iunrnmptss  32851  fcoinvbr  32891  2ndresdju  32935  fmptcof2  32943  acunirnmpt  32945  acunirnmpt2  32946  acunirnmpt2f  32947  aciunf1  32949  fnpreimac  32956  fpwrelmapffslem  33018  gsumwrd2dccatlem  33338  1arithidomlem1  33770  1arithidom  33772  fmcncfil  34266  bnj865  35256  bnj1388  35366  bnj1489  35389  fineqvrep  35450  fineqvac  35452  tz9.1regs  35470  satfrnmapom  35761  satf0op  35768  dmopab3rexdif  35796  prv1n  35822  rexxfr3dALT  36030  eldm3  36152  opelco3  36166  elsingles  36307  funpartlem  36333  dfrdg4  36342  linedegen  36534  prodeq12sdv  36619  cbvoprab2vw  36639  cbvoprab13vw  36642  cbvmodavw  36651  cbvopab1davw  36665  cbvopab2davw  36666  cbvoprab2davw  36673  cbvoprab12davw  36676  cbvoprab23davw  36677  cbvoprab13davw  36678  cbvsumdavw  36680  cbvproddavw  36681  cbvsumdavw2  36696  cbvproddavw2  36697  finminlem  36718  filnetlem4  36781  axtco1  36873  axtco1from2  36875  axtco1g  36876  dfttc4lem1  36928  dfttc4  36930  elttcirr  36931  ttcexg  36932  regsfromregtco  36938  mh-regprimbi  36945  mh-infprim1bi  36946  mobidvALT  37381  bj-issetwt  37399  bj-axreprepsep  37600  bj-restuni  37627  bj-finsumval0  37817  csboprabg  37864  topdifinffinlem  37881  cbveud  37906  wl-sb8eut  38121  wl-sb8eutv  38122  sdclem1  38282  fdc  38284  ismgmOLD  38389  isriscg  38523  elrnres  38817  eldm4  38820  exan3  38839  exanres  38840  eldmcnv  38884  brxrn  38922  exeupre  39030  cosseq  39055  brcoss  39060  brcoss3  39062  eldm1cossres  39089  brcosscnv  39101  islshpat  39681  lshpsmreu  39773  isopos  39844  islpln5  40199  islvol5  40243  pmapjat1  40517  dibelval3  41811  diblsmopel  41835  mapdpglem3  42339  hdmapglem7a  42591  19.9dev  42876  fimgmcyc  43194  dfac11  43681  nnoeomeqom  43931  clcnvlem  44241  dfhe3  44393  ntrneineine0lem  44701  iotasbc  45021  iotasbc2  45022  brpermmodel  45604  permaxinf2lem  45613  permac8prim  45615  nregmodel  45618  fnchoice  45641  axccdom  45830  axccd  45836  stoweidlem35  46641  stoweidlem39  46645  dfatdmfcoafv2  47880  dfatco  47882  ichexmpl1  48107  ichnreuop  48110  ichreuopeq  48111  elsprel  48113  isgrim  48536  dfgric2  48569  gricushgr  48571  gricuspgr  48572  ushggricedg  48581  isubgrgrim  48583  uhgrimisgrgric  48585  grtri  48594  grtriprop  48595  isgrtri  48597  uspgrlim  48646  grlimedgclnbgr  48649  grlimgrtri  48657  dfgrlic2  48662  dfgrlic3  48664  grilcbri2  48665  map0cor  49518  nelsubc3lem  49733  thinccic  50134  istermc  50137  termcpropd  50166  discsntermlem  50233  basrestermcfolem  50234  discsnterm  50237  cnelsubclem  50266  bnd2d  50344