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  32592  fmptcof2  32600  acunirnmpt  32602  acunirnmpt2  32603  acunirnmpt2f  32604  aciunf1  32606  fnpreimac  32614  fpwrelmapffslem  32675  gsumwrd2dccatlem  33019  1arithidomlem1  33472  1arithidom  33474  fmcncfil  33898  bnj865  34890  bnj1388  35000  bnj1489  35023  tz9.1regs  35067  fineqvrep  35070  fineqvac  35072  satfrnmapom  35347  satf0op  35354  dmopab3rexdif  35382  prv1n  35408  rexxfr3dALT  35616  eldm3  35738  opelco3  35752  elsingles  35896  funpartlem  35920  dfrdg4  35929  linedegen  36121  prodeq12sdv  36196  cbvoprab2vw  36216  cbvoprab13vw  36219  cbvmodavw  36228  cbvopab1davw  36242  cbvopab2davw  36243  cbvoprab2davw  36250  cbvoprab12davw  36253  cbvoprab23davw  36254  cbvoprab13davw  36255  cbvsumdavw  36257  cbvproddavw  36258  cbvsumdavw2  36273  cbvproddavw2  36274  finminlem  36296  filnetlem4  36359  mobidvALT  36835  bj-issetwt  36853  bj-restuni  37075  bj-finsumval0  37263  csboprabg  37308  topdifinffinlem  37325  cbveud  37350  wl-sb8eut  37556  wl-sb8eutv  37557  sdclem1  37727  fdc  37729  ismgmOLD  37834  isriscg  37968  elrnres  38250  eldm4  38253  exan3  38272  exanres  38273  eldmcnv  38317  brxrn  38346  cosseq  38407  brcoss  38412  brcoss3  38414  eldm1cossres  38441  brcosscnv  38453  islshpat  39000  lshpsmreu  39092  isopos  39163  islpln5  39518  islvol5  39562  pmapjat1  39836  dibelval3  41130  diblsmopel  41154  mapdpglem3  41658  hdmapglem7a  41910  19.9dev  42191  fimgmcyc  42511  dfac11  43039  nnoeomeqom  43289  clcnvlem  43600  dfhe3  43752  ntrneineine0lem  44060  iotasbc  44396  iotasbc2  44397  brpermmodel  44981  permaxinf2lem  44990  permac8prim  44992  nregmodel  44995  fnchoice  45011  axccdom  45204  axccd  45211  stoweidlem35  46020  stoweidlem39  46024  dfatdmfcoafv2  47242  dfatco  47244  ichexmpl1  47457  ichnreuop  47460  ichreuopeq  47461  elsprel  47463  isgrim  47870  dfgric2  47903  gricushgr  47905  gricuspgr  47906  ushggricedg  47915  isubgrgrim  47917  uhgrimisgrgric  47919  grtri  47928  grtriprop  47929  isgrtri  47931  uspgrlim  47980  grlimedgclnbgr  47983  grlimgrtri  47991  dfgrlic2  47996  dfgrlic3  47998  grilcbri2  47999  map0cor  48843  nelsubc3lem  49059  thinccic  49460  istermc  49463  termcpropd  49492  discsntermlem  49559  basrestermcfolem  49560  discsnterm  49563  cnelsubclem  49592  bnd2d  49670