Theorem exbidv 1918

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

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  nfbidv  1919  2exbidv  1921  3exbidv  1922  eleq1w  2821  eleq2w  2822  eleq1d  2823  eleq2dALT  2825  clelab  2884  rexbidv2  3172  rmoeq1  3413  cgsex4gOLD  3526  ceqsex2  3534  ceqsex2v  3535  alexeqg  3650  sbc2or  3799  sbc5ALT  3819  sbcex2  3855  sbcabel  3886  elpreqprlem  4870  elpreqpr  4871  eluni  4914  csbuni  4940  intab  4982  cbvopab1  5222  cbvopab1g  5223  cbvopab1s  5225  cbvopab1v  5226  axrep1  5285  axreplem  5286  zfrepclf  5296  axsepg  5302  zfauscl  5303  sels  5448  euotd  5522  opeliunxp  5755  brcog  5879  elrn2g  5903  dfdmf  5909  eldmg  5911  dmopabelb  5929  dmopab2rex  5930  dfrnf  5963  elrnmpt1  5973  brcodir  6141  dfco2a  6267  cores  6270  sbcfung  6591  brprcneu  6896  brprcneuALT  6897  ssimaexg  6994  dmfco  7004  fndmdif  7061  fmptco  7148  fliftf  7334  imaeqsexvOLD  7382  oprabbidv  7498  cbvoprab1  7519  cbvoprab2  7520  cbvoprab12v  7522  imaeqexov  7670  uniuni  7780  dmtpos  8261  frecseq123  8305  csbfrecsg  8307  frrlem1  8309  frrlem13  8321  wrecseq123OLD  8338  wfrlem1OLD  8346  wfrlem3OLDa  8349  wfrlem15OLD  8361  rdglim2  8470  ecdmn0  8792  mapsnd  8924  breng  8992  brdom2g  8994  brdomgOLD  8996  domeng  9001  mapsnend  9074  isinf  9293  isinfOLD  9294  ac6sfi  9317  ordiso  9553  brwdom  9604  brwdom2  9610  zfregcl  9631  inf0  9658  zfinf  9676  ttrcleq  9746  brttrcl  9750  brttrcl2  9751  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  ttrclselem2  9763  bnd2  9930  isinffi  10029  acneq  10080  acni  10082  aceq0  10155  aceq3lem  10157  dfac3  10158  dfac5lem4  10163  dfac5lem4OLD  10165  dfac8  10173  dfac9  10174  kmlem1  10188  kmlem2  10189  kmlem8  10195  kmlem10  10197  kmlem13  10200  cfval  10284  cardcf  10289  cfeq0  10293  cfsuc  10294  cff1  10295  cflim3  10299  cofsmo  10306  isfin4  10334  axcc2lem  10473  axcc4dom  10478  domtriomlem  10479  dcomex  10484  axdc2lem  10485  axdc4lem  10492  zfac  10497  ac7g  10511  ac4c  10513  ac5  10514  ac6sg  10525  weth  10532  axrepndlem1  10629  axunndlem1  10632  zfcndrep  10651  zfcndinf  10655  zfcndac  10656  gruina  10855  grothomex  10866  genpass  11046  1idpr  11066  ltexprlem3  11075  ltexprlem4  11076  ltexpri  11080  reclem2pr  11085  reclem3pr  11086  recexpr  11088  infm3  12224  nnunb  12519  axdc4uz  14021  ishashinf  14498  relexpindlem  15098  sumeq1  15721  sumeq2w  15724  sumeq2ii  15725  sumeq2sdv  15735  summo  15749  fsum  15752  fsum2dlem  15802  ntrivcvgn0  15930  ntrivcvgmullem  15933  prodeq1f  15938  prodeq1  15939  prodeq2w  15942  prodeq2ii  15943  prodeq2sdv  15955  prodmo  15968  zprod  15969  fprod  15973  fprodntriv  15974  fprod2dlem  16012  vdwapun  17007  vdwmc  17011  vdwmc2  17012  isacs  17695  dfiso2  17819  brssc  17861  isssc  17867  equivestrcsetc  18207  dirge  18660  gsumvalx  18701  gsumpropd  18703  gsumpropd2lem  18704  gsumress  18707  gsumval3eu  19936  gsumval3lem2  19938  dprd2d2  20078  znleval  21590  neitr  23203  cmpcovf  23414  hausmapdom  23523  ptval  23593  elpt  23595  ptpjopn  23635  ptclsg  23638  ptcnp  23645  uffix2  23947  cnextf  24089  prdsxmslem2  24557  metustfbas  24585  metcld2  25354  dchrmusumlema  27551  dchrisum0lema  27572  elold  27922  lrrecfr  27990  istrkgld  28481  uvtx01vtx  29428  1loopgrvd2  29535  wspthsn  29877  iswspthn  29878  wspthsnon  29881  iswspthsnon  29885  wspthnon  29887  wlkiswwlks2  29904  wlkiswwlksupgr2  29906  wlklnwwlkln2lem  29911  wlksnwwlknvbij  29937  wspthsnwspthsnon  29945  elwwlks2on  29988  elwwlks2  29995  elwspths2spth  29996  clwlkclwwlk  30030  clwwlkvbij  30141  isgrpo  30525  adjeu  31917  iunrnmptss  32585  fcoinvbr  32624  2ndresdju  32665  fmptcof2  32673  acunirnmpt  32675  acunirnmpt2  32676  acunirnmpt2f  32677  aciunf1  32679  fnpreimac  32687  fpwrelmapffslem  32749  gsumwrd2dccatlem  33051  1arithidomlem1  33542  1arithidom  33544  fmcncfil  33891  bnj865  34915  bnj1388  35025  bnj1489  35048  fineqvrep  35087  fineqvac  35089  satfrnmapom  35354  satf0op  35361  dmopab3rexdif  35389  prv1n  35415  rexxfr3dALT  35623  eldm3  35740  opelco3  35755  elsingles  35899  funpartlem  35923  dfrdg4  35932  linedegen  36124  prodeq12sdv  36200  cbvoprab2vw  36220  cbvoprab13vw  36223  cbvmodavw  36232  cbvopab1davw  36246  cbvopab2davw  36247  cbvoprab2davw  36254  cbvoprab12davw  36257  cbvoprab23davw  36258  cbvoprab13davw  36259  cbvsumdavw  36261  cbvproddavw  36262  cbvsumdavw2  36277  cbvproddavw2  36278  finminlem  36300  filnetlem4  36363  mobidvALT  36839  bj-issetwt  36857  bj-restuni  37079  bj-finsumval0  37267  csboprabg  37312  topdifinffinlem  37329  cbveud  37354  wl-sb8eut  37558  wl-sb8eutv  37559  sdclem1  37729  fdc  37731  ismgmOLD  37836  isriscg  37970  elrnres  38252  eldm4  38255  exan3  38275  exanres  38276  eldmcnv  38326  brxrn  38355  cosseq  38407  brcoss  38412  brcoss3  38414  eldm1cossres  38441  brcosscnv  38453  islshpat  38998  lshpsmreu  39090  isopos  39161  islpln5  39517  islvol5  39561  pmapjat1  39835  dibelval3  41129  diblsmopel  41153  mapdpglem3  41657  hdmapglem7a  41909  19.9dev  42231  fimgmcyc  42520  dfac11  43050  nnoeomeqom  43301  clcnvlem  43612  dfhe3  43764  ntrneineine0lem  44072  iotasbc  44414  iotasbc2  44415  fnchoice  44966  axccdom  45164  axccd  45171  stoweidlem35  45990  stoweidlem39  45994  dfatdmfcoafv2  47203  dfatco  47205  ichexmpl1  47393  ichnreuop  47396  ichreuopeq  47397  elsprel  47399  isgrim  47805  dfgric2  47821  gricushgr  47823  gricuspgr  47824  ushggricedg  47833  isubgrgrim  47834  uhgrimisgrgric  47836  grtri  47844  grtriprop  47845  isgrtri  47847  uspgrlim  47894  grlimgrtri  47898  dfgrlic2  47903  dfgrlic3  47905  grilcbri2  47906  opeliun2xp  48177  map0cor  48684  thinccic  48861  bnd2d  48911