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  3149  rmoeq1  3376  cgsex4gOLD  3484  ceqsex2  3490  ceqsex2v  3491  alexeqg  3606  sbc2or  3751  sbc5ALT  3771  sbcex2  3803  sbcabel  3830  elpreqprlem  4817  elpreqpr  4818  eluni  4861  csbuni  4887  intab  4928  cbvopab1  5166  cbvopab1g  5167  cbvopab1s  5169  cbvopab1v  5170  axrep1  5219  axreplem  5220  zfrepclf  5230  axsepg  5236  zfauscl  5237  sels  5382  euotd  5456  opeliunxp  5686  opeliun2xp  5687  brcog  5809  elrn2g  5833  dfdmf  5839  eldmg  5841  dmopabelb  5859  dmopab2rex  5860  dfrnf  5892  elrnmpt1  5902  brcodir  6068  dfco2a  6195  cores  6198  sbcfung  6506  brprcneu  6812  brprcneuALT  6813  ssimaexg  6909  dmfco  6919  fndmdif  6976  fmptco  7063  fliftf  7252  imaeqsexvOLD  7300  oprabbidv  7415  cbvoprab1  7436  cbvoprab2  7437  cbvoprab12v  7439  imaeqexov  7587  uniuni  7698  dmtpos  8171  frecseq123  8215  csbfrecsg  8217  frrlem1  8219  frrlem13  8231  rdglim2  8354  ecdmn0  8677  mapsnd  8813  breng  8881  brdom2g  8883  domeng  8888  mapsnend  8961  isinf  9154  ac6sfi  9173  ordiso  9408  brwdom  9459  brwdom2  9465  zfregcl  9486  zfregclOLD  9487  inf0  9517  zfinf  9535  ttrcleq  9605  brttrcl  9609  brttrcl2  9610  ssttrcl  9611  ttrcltr  9612  ttrclss  9616  ttrclselem2  9622  bnd2  9789  isinffi  9888  acneq  9937  acni  9939  aceq0  10012  aceq3lem  10014  dfac3  10015  dfac5lem4  10020  dfac5lem4OLD  10022  dfac8  10030  dfac9  10031  kmlem1  10045  kmlem2  10046  kmlem8  10052  kmlem10  10054  kmlem13  10057  cfval  10141  cardcf  10146  cfeq0  10150  cfsuc  10151  cff1  10152  cflim3  10156  cofsmo  10163  isfin4  10191  axcc2lem  10330  axcc4dom  10335  domtriomlem  10336  dcomex  10341  axdc2lem  10342  axdc4lem  10349  zfac  10354  ac7g  10368  ac4c  10370  ac5  10371  ac6sg  10382  weth  10389  axrepndlem1  10486  axunndlem1  10489  zfcndrep  10508  zfcndinf  10512  zfcndac  10513  gruina  10712  grothomex  10723  genpass  10903  1idpr  10923  ltexprlem3  10932  ltexprlem4  10933  ltexpri  10937  reclem2pr  10942  reclem3pr  10943  recexpr  10945  infm3  12084  nnunb  12380  axdc4uz  13891  ishashinf  14370  relexpindlem  14970  sumeq1  15596  sumeq2w  15599  sumeq2ii  15600  sumeq2sdv  15610  summo  15624  fsum  15627  fsum2dlem  15677  ntrivcvgn0  15805  ntrivcvgmullem  15808  prodeq1f  15813  prodeq1  15814  prodeq2w  15817  prodeq2ii  15818  prodeq2sdv  15830  prodmo  15843  zprod  15844  fprod  15848  fprodntriv  15849  fprod2dlem  15887  vdwapun  16886  vdwmc  16890  vdwmc2  16891  isacs  17557  dfiso2  17679  brssc  17721  isssc  17727  equivestrcsetc  18058  dirge  18509  gsumvalx  18550  gsumpropd  18552  gsumpropd2lem  18553  gsumress  18556  gsumval3eu  19783  gsumval3lem2  19785  dprd2d2  19925  znleval  21461  neitr  23065  cmpcovf  23276  hausmapdom  23385  ptval  23455  elpt  23457  ptpjopn  23497  ptclsg  23500  ptcnp  23507  uffix2  23809  cnextf  23951  prdsxmslem2  24415  metustfbas  24443  metcld2  25205  dchrmusumlema  27402  dchrisum0lema  27423  elold  27783  lrrecfr  27855  istrkgld  28404  uvtx01vtx  29342  1loopgrvd2  29449  wspthsn  29793  iswspthn  29794  wspthsnon  29797  iswspthsnon  29801  wspthnon  29803  wlkiswwlks2  29820  wlkiswwlksupgr2  29822  wlklnwwlkln2lem  29827  wlksnwwlknvbij  29853  wspthsnwspthsnon  29861  elwwlks2on  29904  elwwlks2  29911  elwspths2spth  29912  clwlkclwwlk  29946  clwwlkvbij  30057  isgrpo  30441  adjeu  31833  iunrnmptss  32509  fcoinvbr  32549  2ndresdju  32593  fmptcof2  32601  acunirnmpt  32603  acunirnmpt2  32604  acunirnmpt2f  32605  aciunf1  32607  fnpreimac  32615  fpwrelmapffslem  32676  gsumwrd2dccatlem  33020  1arithidomlem1  33473  1arithidom  33475  fmcncfil  33904  bnj865  34896  bnj1388  35006  bnj1489  35029  tz9.1regs  35073  fineqvrep  35076  fineqvac  35078  satfrnmapom  35353  satf0op  35360  dmopab3rexdif  35388  prv1n  35414  rexxfr3dALT  35622  eldm3  35744  opelco3  35758  elsingles  35902  funpartlem  35926  dfrdg4  35935  linedegen  36127  prodeq12sdv  36202  cbvoprab2vw  36222  cbvoprab13vw  36225  cbvmodavw  36234  cbvopab1davw  36248  cbvopab2davw  36249  cbvoprab2davw  36256  cbvoprab12davw  36259  cbvoprab23davw  36260  cbvoprab13davw  36261  cbvsumdavw  36263  cbvproddavw  36264  cbvsumdavw2  36279  cbvproddavw2  36280  finminlem  36302  filnetlem4  36365  mobidvALT  36841  bj-issetwt  36859  bj-restuni  37081  bj-finsumval0  37269  csboprabg  37314  topdifinffinlem  37331  cbveud  37356  wl-sb8eut  37562  wl-sb8eutv  37563  sdclem1  37733  fdc  37735  ismgmOLD  37840  isriscg  37974  elrnres  38256  eldm4  38259  exan3  38278  exanres  38279  eldmcnv  38323  brxrn  38352  cosseq  38413  brcoss  38418  brcoss3  38420  eldm1cossres  38447  brcosscnv  38459  islshpat  39006  lshpsmreu  39098  isopos  39169  islpln5  39524  islvol5  39568  pmapjat1  39842  dibelval3  41136  diblsmopel  41160  mapdpglem3  41664  hdmapglem7a  41916  19.9dev  42197  fimgmcyc  42517  dfac11  43045  nnoeomeqom  43295  clcnvlem  43606  dfhe3  43758  ntrneineine0lem  44066  iotasbc  44402  iotasbc2  44403  brpermmodel  44987  permaxinf2lem  44996  permac8prim  44998  nregmodel  45001  fnchoice  45017  axccdom  45210  axccd  45217  stoweidlem35  46026  stoweidlem39  46030  dfatdmfcoafv2  47248  dfatco  47250  ichexmpl1  47463  ichnreuop  47466  ichreuopeq  47467  elsprel  47469  isgrim  47876  dfgric2  47909  gricushgr  47911  gricuspgr  47912  ushggricedg  47921  isubgrgrim  47923  uhgrimisgrgric  47925  grtri  47934  grtriprop  47935  isgrtri  47937  uspgrlim  47986  grlimedgclnbgr  47989  grlimgrtri  47997  dfgrlic2  48002  dfgrlic3  48004  grilcbri2  48005  map0cor  48849  nelsubc3lem  49065  thinccic  49466  istermc  49469  termcpropd  49498  discsntermlem  49565  basrestermcfolem  49566  discsnterm  49569  cnelsubclem  49598  bnd2d  49676