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  2811  eleq2w  2812  eleq1d  2813  eleq2dALT  2815  clelab  2873  rexbidv2  3153  rmoeq1  3387  cgsex4gOLD  3495  ceqsex2  3501  ceqsex2v  3502  alexeqg  3617  sbc2or  3762  sbc5ALT  3782  sbcex2  3814  sbcabel  3841  elpreqprlem  4830  elpreqpr  4831  eluni  4874  csbuni  4900  intab  4942  cbvopab1  5181  cbvopab1g  5182  cbvopab1s  5184  cbvopab1v  5185  axrep1  5235  axreplem  5236  zfrepclf  5246  axsepg  5252  zfauscl  5253  sels  5398  euotd  5473  opeliunxp  5705  opeliun2xp  5706  brcog  5830  elrn2g  5854  dfdmf  5860  eldmg  5862  dmopabelb  5880  dmopab2rex  5881  dfrnf  5914  elrnmpt1  5924  brcodir  6092  dfco2a  6219  cores  6222  sbcfung  6540  brprcneu  6848  brprcneuALT  6849  ssimaexg  6947  dmfco  6957  fndmdif  7014  fmptco  7101  fliftf  7290  imaeqsexvOLD  7338  oprabbidv  7455  cbvoprab1  7476  cbvoprab2  7477  cbvoprab12v  7479  imaeqexov  7627  uniuni  7738  dmtpos  8217  frecseq123  8261  csbfrecsg  8263  frrlem1  8265  frrlem13  8277  rdglim2  8400  ecdmn0  8723  mapsnd  8859  breng  8927  brdom2g  8929  domeng  8934  mapsnend  9007  isinf  9207  isinfOLD  9208  ac6sfi  9231  ordiso  9469  brwdom  9520  brwdom2  9526  zfregcl  9547  inf0  9574  zfinf  9592  ttrcleq  9662  brttrcl  9666  brttrcl2  9667  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  bnd2  9846  isinffi  9945  acneq  9996  acni  9998  aceq0  10071  aceq3lem  10073  dfac3  10074  dfac5lem4  10079  dfac5lem4OLD  10081  dfac8  10089  dfac9  10090  kmlem1  10104  kmlem2  10105  kmlem8  10111  kmlem10  10113  kmlem13  10116  cfval  10200  cardcf  10205  cfeq0  10209  cfsuc  10210  cff1  10211  cflim3  10215  cofsmo  10222  isfin4  10250  axcc2lem  10389  axcc4dom  10394  domtriomlem  10395  dcomex  10400  axdc2lem  10401  axdc4lem  10408  zfac  10413  ac7g  10427  ac4c  10429  ac5  10430  ac6sg  10441  weth  10448  axrepndlem1  10545  axunndlem1  10548  zfcndrep  10567  zfcndinf  10571  zfcndac  10572  gruina  10771  grothomex  10782  genpass  10962  1idpr  10982  ltexprlem3  10991  ltexprlem4  10992  ltexpri  10996  reclem2pr  11001  reclem3pr  11002  recexpr  11004  infm3  12142  nnunb  12438  axdc4uz  13949  ishashinf  14428  relexpindlem  15029  sumeq1  15655  sumeq2w  15658  sumeq2ii  15659  sumeq2sdv  15669  summo  15683  fsum  15686  fsum2dlem  15736  ntrivcvgn0  15864  ntrivcvgmullem  15867  prodeq1f  15872  prodeq1  15873  prodeq2w  15876  prodeq2ii  15877  prodeq2sdv  15889  prodmo  15902  zprod  15903  fprod  15907  fprodntriv  15908  fprod2dlem  15946  vdwapun  16945  vdwmc  16949  vdwmc2  16950  isacs  17612  dfiso2  17734  brssc  17776  isssc  17782  equivestrcsetc  18113  dirge  18562  gsumvalx  18603  gsumpropd  18605  gsumpropd2lem  18606  gsumress  18609  gsumval3eu  19834  gsumval3lem2  19836  dprd2d2  19976  znleval  21464  neitr  23067  cmpcovf  23278  hausmapdom  23387  ptval  23457  elpt  23459  ptpjopn  23499  ptclsg  23502  ptcnp  23509  uffix2  23811  cnextf  23953  prdsxmslem2  24417  metustfbas  24445  metcld2  25207  dchrmusumlema  27404  dchrisum0lema  27425  elold  27781  lrrecfr  27850  istrkgld  28386  uvtx01vtx  29324  1loopgrvd2  29431  wspthsn  29778  iswspthn  29779  wspthsnon  29782  iswspthsnon  29786  wspthnon  29788  wlkiswwlks2  29805  wlkiswwlksupgr2  29807  wlklnwwlkln2lem  29812  wlksnwwlknvbij  29838  wspthsnwspthsnon  29846  elwwlks2on  29889  elwwlks2  29896  elwspths2spth  29897  clwlkclwwlk  29931  clwwlkvbij  30042  isgrpo  30426  adjeu  31818  iunrnmptss  32494  fcoinvbr  32534  2ndresdju  32573  fmptcof2  32581  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1  32587  fnpreimac  32595  fpwrelmapffslem  32655  gsumwrd2dccatlem  33006  1arithidomlem1  33506  1arithidom  33508  fmcncfil  33921  bnj865  34913  bnj1388  35023  bnj1489  35046  fineqvrep  35085  fineqvac  35087  satfrnmapom  35357  satf0op  35364  dmopab3rexdif  35392  prv1n  35418  rexxfr3dALT  35626  eldm3  35748  opelco3  35762  elsingles  35906  funpartlem  35930  dfrdg4  35939  linedegen  36131  prodeq12sdv  36206  cbvoprab2vw  36226  cbvoprab13vw  36229  cbvmodavw  36238  cbvopab1davw  36252  cbvopab2davw  36253  cbvoprab2davw  36260  cbvoprab12davw  36263  cbvoprab23davw  36264  cbvoprab13davw  36265  cbvsumdavw  36267  cbvproddavw  36268  cbvsumdavw2  36283  cbvproddavw2  36284  finminlem  36306  filnetlem4  36369  mobidvALT  36845  bj-issetwt  36863  bj-restuni  37085  bj-finsumval0  37273  csboprabg  37318  topdifinffinlem  37335  cbveud  37360  wl-sb8eut  37566  wl-sb8eutv  37567  sdclem1  37737  fdc  37739  ismgmOLD  37844  isriscg  37978  elrnres  38260  eldm4  38263  exan3  38282  exanres  38283  eldmcnv  38327  brxrn  38356  cosseq  38417  brcoss  38422  brcoss3  38424  eldm1cossres  38451  brcosscnv  38463  islshpat  39010  lshpsmreu  39102  isopos  39173  islpln5  39529  islvol5  39573  pmapjat1  39847  dibelval3  41141  diblsmopel  41165  mapdpglem3  41669  hdmapglem7a  41921  19.9dev  42202  fimgmcyc  42522  dfac11  43051  nnoeomeqom  43301  clcnvlem  43612  dfhe3  43764  ntrneineine0lem  44072  iotasbc  44408  iotasbc2  44409  brpermmodel  44993  permaxinf2lem  45002  permac8prim  45004  nregmodel  45007  fnchoice  45023  axccdom  45216  axccd  45223  stoweidlem35  46033  stoweidlem39  46037  dfatdmfcoafv2  47255  dfatco  47257  ichexmpl1  47470  ichnreuop  47473  ichreuopeq  47474  elsprel  47476  isgrim  47882  dfgric2  47915  gricushgr  47917  gricuspgr  47918  ushggricedg  47927  isubgrgrim  47929  uhgrimisgrgric  47931  grtri  47939  grtriprop  47940  isgrtri  47942  uspgrlim  47991  grlimgrtri  47995  dfgrlic2  48000  dfgrlic3  48002  grilcbri2  48003  map0cor  48843  nelsubc3lem  49059  thinccic  49460  istermc  49463  termcpropd  49492  discsntermlem  49559  basrestermcfolem  49560  discsnterm  49563  cnelsubclem  49592  bnd2d  49670