Theorem exbidv 1922

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  nfbidv  1923  2exbidv  1925  3exbidv  1926  eleq1w  2819  eleq2w  2820  eleq1d  2821  eleq2dALT  2823  clelab  2880  rexbidv2  3156  rmoeq1  3381  cgsex4gOLD  3488  ceqsex2  3493  ceqsex2v  3494  alexeqg  3605  sbc2or  3749  sbc5ALT  3769  sbcex2  3801  sbcabel  3828  elpreqprlem  4822  elpreqpr  4823  eluni  4866  csbuni  4893  intab  4933  cbvopab1  5172  cbvopab1g  5173  cbvopab1s  5175  cbvopab1v  5176  axrep1  5225  axreplem  5226  zfrepclf  5236  axsepg  5242  zfauscl  5243  sels  5388  euotd  5461  opeliunxp  5691  opeliun2xp  5692  brcog  5815  elrn2g  5839  dfdmf  5845  eldmg  5847  dmun  5859  dmopabelb  5865  dmopab2rex  5866  dm0rn0  5873  dfrnf  5899  elrnmpt1  5909  brcodir  6076  dfco2a  6204  cores  6207  sbcfung  6516  brprcneu  6824  brprcneuALT  6825  ssimaexg  6920  dmfco  6930  fndmdif  6987  fmptco  7074  fliftf  7261  imaeqsexvOLD  7309  oprabbidv  7424  cbvoprab1  7445  cbvoprab2  7446  cbvoprab12v  7448  imaeqexov  7596  uniuni  7707  dmtpos  8180  frecseq123  8224  csbfrecsg  8226  frrlem1  8228  frrlem13  8240  rdglim2  8363  ecdmn0  8687  mapsnd  8824  breng  8892  brdom2g  8894  domeng  8899  mapsnend  8973  isinf  9165  ac6sfi  9184  ordiso  9421  brwdom  9472  brwdom2  9478  zfregcl  9499  zfregclOLD  9500  inf0  9530  zfinf  9548  ttrcleq  9618  brttrcl  9622  brttrcl2  9623  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  bnd2  9805  isinffi  9904  acneq  9953  acni  9955  aceq0  10028  aceq3lem  10030  dfac3  10031  dfac5lem4  10036  dfac5lem4OLD  10038  dfac8  10046  dfac9  10047  kmlem1  10061  kmlem2  10062  kmlem8  10068  kmlem10  10070  kmlem13  10073  cfval  10157  cardcf  10162  cfeq0  10166  cfsuc  10167  cff1  10168  cflim3  10172  cofsmo  10179  isfin4  10207  axcc2lem  10346  axcc4dom  10351  domtriomlem  10352  dcomex  10357  axdc2lem  10358  axdc4lem  10365  zfac  10370  ac7g  10384  ac4c  10386  ac5  10387  ac6sg  10398  weth  10405  axrepndlem1  10503  axunndlem1  10506  zfcndrep  10525  zfcndinf  10529  zfcndac  10530  gruina  10729  grothomex  10740  genpass  10920  1idpr  10940  ltexprlem3  10949  ltexprlem4  10950  ltexpri  10954  reclem2pr  10959  reclem3pr  10960  recexpr  10962  infm3  12101  nnunb  12397  axdc4uz  13907  ishashinf  14386  relexpindlem  14986  sumeq1  15612  sumeq2w  15615  sumeq2ii  15616  sumeq2sdv  15626  summo  15640  fsum  15643  fsum2dlem  15693  ntrivcvgn0  15821  ntrivcvgmullem  15824  prodeq1f  15829  prodeq1  15830  prodeq2w  15833  prodeq2ii  15834  prodeq2sdv  15846  prodmo  15859  zprod  15860  fprod  15864  fprodntriv  15865  fprod2dlem  15903  vdwapun  16902  vdwmc  16906  vdwmc2  16907  isacs  17574  dfiso2  17696  brssc  17738  isssc  17744  equivestrcsetc  18075  dirge  18526  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  gsumval3eu  19833  gsumval3lem2  19835  dprd2d2  19975  znleval  21509  neitr  23124  cmpcovf  23335  hausmapdom  23444  ptval  23514  elpt  23516  ptpjopn  23556  ptclsg  23559  ptcnp  23566  uffix2  23868  cnextf  24010  prdsxmslem2  24473  metustfbas  24501  metcld2  25263  dchrmusumlema  27460  dchrisum0lema  27481  elold  27855  lrrecfr  27939  istrkgld  28531  uvtx01vtx  29470  1loopgrvd2  29577  wspthsn  29921  iswspthn  29922  wspthsnon  29925  iswspthsnon  29929  wspthnon  29931  wlkiswwlks2  29948  wlkiswwlksupgr2  29950  wlklnwwlkln2lem  29955  wlksnwwlknvbij  29981  wspthsnwspthsnon  29989  elwwlks2on  30034  elwwlks2  30042  elwspths2spth  30043  clwlkclwwlk  30077  clwwlkvbij  30188  isgrpo  30572  adjeu  31964  iunrnmptss  32640  fcoinvbr  32680  2ndresdju  32727  fmptcof2  32735  acunirnmpt  32737  acunirnmpt2  32738  acunirnmpt2f  32739  aciunf1  32741  fnpreimac  32749  fpwrelmapffslem  32811  gsumwrd2dccatlem  33159  1arithidomlem1  33616  1arithidom  33618  fmcncfil  34088  bnj865  35079  bnj1388  35189  bnj1489  35212  fineqvrep  35270  fineqvac  35272  tz9.1regs  35290  satfrnmapom  35564  satf0op  35571  dmopab3rexdif  35599  prv1n  35625  rexxfr3dALT  35833  eldm3  35955  opelco3  35969  elsingles  36110  funpartlem  36136  dfrdg4  36145  linedegen  36337  prodeq12sdv  36412  cbvoprab2vw  36432  cbvoprab13vw  36435  cbvmodavw  36444  cbvopab1davw  36458  cbvopab2davw  36459  cbvoprab2davw  36466  cbvoprab12davw  36469  cbvoprab23davw  36470  cbvoprab13davw  36471  cbvsumdavw  36473  cbvproddavw  36474  cbvsumdavw2  36489  cbvproddavw2  36490  finminlem  36512  filnetlem4  36575  regsfromregtr  36668  mobidvALT  37058  bj-issetwt  37076  bj-restuni  37302  bj-finsumval0  37490  csboprabg  37535  topdifinffinlem  37552  cbveud  37577  wl-sb8eut  37783  wl-sb8eutv  37784  sdclem1  37944  fdc  37946  ismgmOLD  38051  isriscg  38185  elrnres  38473  eldm4  38476  exan3  38495  exanres  38496  eldmcnv  38540  brxrn  38578  exeupre  38674  cosseq  38699  brcoss  38704  brcoss3  38706  eldm1cossres  38733  brcosscnv  38745  islshpat  39287  lshpsmreu  39379  isopos  39450  islpln5  39805  islvol5  39849  pmapjat1  40123  dibelval3  41417  diblsmopel  41441  mapdpglem3  41945  hdmapglem7a  42197  19.9dev  42481  fimgmcyc  42799  dfac11  43314  nnoeomeqom  43564  clcnvlem  43874  dfhe3  44026  ntrneineine0lem  44334  iotasbc  44670  iotasbc2  44671  brpermmodel  45254  permaxinf2lem  45263  permac8prim  45265  nregmodel  45268  fnchoice  45284  axccdom  45476  axccd  45483  stoweidlem35  46289  stoweidlem39  46293  dfatdmfcoafv2  47510  dfatco  47512  ichexmpl1  47725  ichnreuop  47728  ichreuopeq  47729  elsprel  47731  isgrim  48138  dfgric2  48171  gricushgr  48173  gricuspgr  48174  ushggricedg  48183  isubgrgrim  48185  uhgrimisgrgric  48187  grtri  48196  grtriprop  48197  isgrtri  48199  uspgrlim  48248  grlimedgclnbgr  48251  grlimgrtri  48259  dfgrlic2  48264  dfgrlic3  48266  grilcbri2  48267  map0cor  49110  nelsubc3lem  49325  thinccic  49726  istermc  49729  termcpropd  49758  discsntermlem  49825  basrestermcfolem  49826  discsnterm  49829  cnelsubclem  49858  bnd2d  49936