Theorem exbidv 1922

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1868 and exbid 2228. (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  2817  eleq2w  2818  eleq1d  2819  eleq2dALT  2821  clelab  2878  rexbidv2  3154  rmoeq1  3379  cgsex4gOLD  3486  ceqsex2  3491  ceqsex2v  3492  alexeqg  3603  sbc2or  3747  sbc5ALT  3767  sbcex2  3799  sbcabel  3826  elpreqprlem  4820  elpreqpr  4821  eluni  4864  csbuni  4891  intab  4931  cbvopab1  5170  cbvopab1g  5171  cbvopab1s  5173  cbvopab1v  5174  axrep1  5223  axreplem  5224  zfrepclf  5234  axsepg  5240  zfauscl  5241  sels  5386  euotd  5459  opeliunxp  5689  opeliun2xp  5690  brcog  5813  elrn2g  5837  dfdmf  5843  eldmg  5845  dmun  5857  dmopabelb  5863  dmopab2rex  5864  dm0rn0  5871  dfrnf  5897  elrnmpt1  5907  brcodir  6074  dfco2a  6202  cores  6205  sbcfung  6514  brprcneu  6822  brprcneuALT  6823  ssimaexg  6918  dmfco  6928  fndmdif  6985  fmptco  7072  fliftf  7259  imaeqsexvOLD  7307  oprabbidv  7422  cbvoprab1  7443  cbvoprab2  7444  cbvoprab12v  7446  imaeqexov  7594  uniuni  7705  dmtpos  8178  frecseq123  8222  csbfrecsg  8224  frrlem1  8226  frrlem13  8238  rdglim2  8361  ecdmn0  8685  mapsnd  8822  breng  8890  brdom2g  8892  domeng  8897  mapsnend  8971  isinf  9163  ac6sfi  9182  ordiso  9419  brwdom  9470  brwdom2  9476  zfregcl  9497  zfregclOLD  9498  inf0  9528  zfinf  9546  ttrcleq  9616  brttrcl  9620  brttrcl2  9621  ssttrcl  9622  ttrcltr  9623  ttrclss  9627  ttrclselem2  9633  bnd2  9803  isinffi  9902  acneq  9951  acni  9953  aceq0  10026  aceq3lem  10028  dfac3  10029  dfac5lem4  10034  dfac5lem4OLD  10036  dfac8  10044  dfac9  10045  kmlem1  10059  kmlem2  10060  kmlem8  10066  kmlem10  10068  kmlem13  10071  cfval  10155  cardcf  10160  cfeq0  10164  cfsuc  10165  cff1  10166  cflim3  10170  cofsmo  10177  isfin4  10205  axcc2lem  10344  axcc4dom  10349  domtriomlem  10350  dcomex  10355  axdc2lem  10356  axdc4lem  10363  zfac  10368  ac7g  10382  ac4c  10384  ac5  10385  ac6sg  10396  weth  10403  axrepndlem1  10501  axunndlem1  10504  zfcndrep  10523  zfcndinf  10527  zfcndac  10528  gruina  10727  grothomex  10738  genpass  10918  1idpr  10938  ltexprlem3  10947  ltexprlem4  10948  ltexpri  10952  reclem2pr  10957  reclem3pr  10958  recexpr  10960  infm3  12099  nnunb  12395  axdc4uz  13905  ishashinf  14384  relexpindlem  14984  sumeq1  15610  sumeq2w  15613  sumeq2ii  15614  sumeq2sdv  15624  summo  15638  fsum  15641  fsum2dlem  15691  ntrivcvgn0  15819  ntrivcvgmullem  15822  prodeq1f  15827  prodeq1  15828  prodeq2w  15831  prodeq2ii  15832  prodeq2sdv  15844  prodmo  15857  zprod  15858  fprod  15862  fprodntriv  15863  fprod2dlem  15901  vdwapun  16900  vdwmc  16904  vdwmc2  16905  isacs  17572  dfiso2  17694  brssc  17736  isssc  17742  equivestrcsetc  18073  dirge  18524  gsumvalx  18599  gsumpropd  18601  gsumpropd2lem  18602  gsumress  18605  gsumval3eu  19831  gsumval3lem2  19833  dprd2d2  19973  znleval  21507  neitr  23122  cmpcovf  23333  hausmapdom  23442  ptval  23512  elpt  23514  ptpjopn  23554  ptclsg  23557  ptcnp  23564  uffix2  23866  cnextf  24008  prdsxmslem2  24471  metustfbas  24499  metcld2  25261  dchrmusumlema  27458  dchrisum0lema  27479  elold  27841  lrrecfr  27913  istrkgld  28480  uvtx01vtx  29419  1loopgrvd2  29526  wspthsn  29870  iswspthn  29871  wspthsnon  29874  iswspthsnon  29878  wspthnon  29880  wlkiswwlks2  29897  wlkiswwlksupgr2  29899  wlklnwwlkln2lem  29904  wlksnwwlknvbij  29930  wspthsnwspthsnon  29938  elwwlks2on  29983  elwwlks2  29991  elwspths2spth  29992  clwlkclwwlk  30026  clwwlkvbij  30137  isgrpo  30521  adjeu  31913  iunrnmptss  32589  fcoinvbr  32629  2ndresdju  32676  fmptcof2  32684  acunirnmpt  32686  acunirnmpt2  32687  acunirnmpt2f  32688  aciunf1  32690  fnpreimac  32698  fpwrelmapffslem  32760  gsumwrd2dccatlem  33108  1arithidomlem1  33565  1arithidom  33567  fmcncfil  34037  bnj865  35028  bnj1388  35138  bnj1489  35161  fineqvrep  35219  fineqvac  35221  tz9.1regs  35239  satfrnmapom  35513  satf0op  35520  dmopab3rexdif  35548  prv1n  35574  rexxfr3dALT  35782  eldm3  35904  opelco3  35918  elsingles  36059  funpartlem  36085  dfrdg4  36094  linedegen  36286  prodeq12sdv  36361  cbvoprab2vw  36381  cbvoprab13vw  36384  cbvmodavw  36393  cbvopab1davw  36407  cbvopab2davw  36408  cbvoprab2davw  36415  cbvoprab12davw  36418  cbvoprab23davw  36419  cbvoprab13davw  36420  cbvsumdavw  36422  cbvproddavw  36423  cbvsumdavw2  36438  cbvproddavw2  36439  finminlem  36461  filnetlem4  36524  mobidvALT  37001  bj-issetwt  37019  bj-restuni  37241  bj-finsumval0  37429  csboprabg  37474  topdifinffinlem  37491  cbveud  37516  wl-sb8eut  37722  wl-sb8eutv  37723  sdclem1  37883  fdc  37885  ismgmOLD  37990  isriscg  38124  elrnres  38410  eldm4  38413  exan3  38432  exanres  38433  eldmcnv  38477  brxrn  38507  exeupre  38603  cosseq  38628  brcoss  38633  brcoss3  38635  eldm1cossres  38662  brcosscnv  38674  islshpat  39216  lshpsmreu  39308  isopos  39379  islpln5  39734  islvol5  39778  pmapjat1  40052  dibelval3  41346  diblsmopel  41370  mapdpglem3  41874  hdmapglem7a  42126  19.9dev  42412  fimgmcyc  42731  dfac11  43246  nnoeomeqom  43496  clcnvlem  43806  dfhe3  43958  ntrneineine0lem  44266  iotasbc  44602  iotasbc2  44603  brpermmodel  45186  permaxinf2lem  45195  permac8prim  45197  nregmodel  45200  fnchoice  45216  axccdom  45408  axccd  45415  stoweidlem35  46221  stoweidlem39  46225  dfatdmfcoafv2  47442  dfatco  47444  ichexmpl1  47657  ichnreuop  47660  ichreuopeq  47661  elsprel  47663  isgrim  48070  dfgric2  48103  gricushgr  48105  gricuspgr  48106  ushggricedg  48115  isubgrgrim  48117  uhgrimisgrgric  48119  grtri  48128  grtriprop  48129  isgrtri  48131  uspgrlim  48180  grlimedgclnbgr  48183  grlimgrtri  48191  dfgrlic2  48196  dfgrlic3  48198  grilcbri2  48199  map0cor  49042  nelsubc3lem  49257  thinccic  49658  istermc  49661  termcpropd  49690  discsntermlem  49757  basrestermcfolem  49758  discsnterm  49761  cnelsubclem  49790  bnd2d  49868