Theorem exbidv 1954

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  nfbidv  1955  2exbidv  1957  3exbidv  1958  eleq1w  2848  eleq2w  2849  eleq1d  2850  eleq2dALT  2852  clelab  2909  rexbidv2  3187  rmoeq1  3402  ceqsex2  3507  ceqsex2v  3508  alexeqg  3612  sbc2or  3755  sbc5ALT  3775  sbcex2  3806  sbcabel  3832  elpreqprlem  4833  elpreqpr  4834  eluni  4877  csbuni  4905  intab  4945  cbvopab1  5187  cbvopab1g  5188  cbvopab1s  5190  cbvopab1v  5191  axrep1  5241  axreplem  5242  zfrepclf  5254  axsepg  5260  sepg  5261  zfausclOLD  5263  sels  5423  euotd  5498  opeliunxp  5730  opeliun2xp  5731  brcog  5854  elrn2g  5882  dfdmf  5888  eldmg  5890  dmun  5902  dmopabelb  5908  dmopab2rex  5909  dm0rn0  5916  dfrnf  5942  elrnmpt1  5952  brcodir  6121  dfco2a  6249  cores  6252  sbcfung  6564  brprcneu  6875  brprcneuALT  6876  ssimaexg  6971  dmfco  6981  fndmdif  7041  fmptco  7129  fliftf  7322  oprabbidv  7485  cbvoprab1  7506  cbvoprab2  7507  cbvoprab12v  7509  imaeqexov  7658  uniuni  7767  dmtpos  8240  frecseq123  8285  csbfrecsg  8287  frrlem1  8289  frrlem13  8301  rdglim2  8425  ecdmn0  8753  mapsnd  8890  breng  8958  brdom2g  8960  domeng  8965  mapsnend  9040  isinf  9232  ac6sfi  9251  ordiso  9485  brwdom  9536  brwdom2  9542  zfregcl  9563  zfregclOLD  9564  inf0  9597  zfinf  9615  ttrcleq  9685  brttrcl  9689  brttrcl2  9690  ssttrcl  9691  ttrcltr  9692  ttrclss  9696  ttrclselem2  9702  bnd2  9892  isinffi  9994  acneq  10043  acni  10045  aceq0  10118  aceq3lem  10120  dfac3  10121  dfac5lem4  10126  dfac8  10135  dfac9  10136  kmlem1  10150  kmlem2  10151  kmlem8  10157  kmlem10  10159  kmlem13  10162  cfval  10245  cardcf  10250  cfeq0  10255  cfsuc  10256  cff1  10257  cflim3  10261  cofsmo  10268  isfin4  10296  axcc2lem  10435  axcc4dom  10440  domtriomlem  10441  dcomex  10446  axdc2lem  10447  axdc4lem  10454  zfac  10459  ac7g  10473  ac4c  10475  ac5  10476  ac6sg  10487  weth  10494  axrepndlem1  10594  axunndlem1  10597  zfcndrep  10616  zfcndinf  10620  zfcndac  10621  gruina  10820  grothomex  10831  genpass  11011  1idpr  11031  ltexprlem3  11040  ltexprlem4  11041  ltexpri  11045  reclem2pr  11050  reclem3pr  11051  recexpr  11053  infm3  12191  nnunb  12517  axdc4uz  14040  ishashinf  14520  relexpindlem  15126  sumeq1  15766  sumeq2w  15769  sumeq2ii  15770  sumeq2sdv  15780  summo  15793  fsum  15796  fsum2dlem  15846  ntrivcvgn0  15977  ntrivcvgmullem  15980  prodeq1f  15985  prodeq1  15986  prodeq2w  15989  prodeq2ii  15990  prodeq2sdv  16002  prodmo  16015  zprod  16016  fprod  16020  fprodntriv  16021  fprod2dlem  16059  vdwapun  17058  vdwmc  17062  vdwmc2  17063  isacs  17731  dfiso2  17853  brssc  17895  isssc  17901  equivestrcsetc  18232  dirge  18683  gsumvalx  18768  gsumpropd  18770  gsumpropd2lem  18771  gsumress  18774  degenmgm2nfun  19041  gsumval3eu  20020  gsumval3lem2  20022  dprd2d2  20162  znleval  21756  neitr  23389  cmpcovf  23600  hausmapdom  23710  ptval  23780  elpt  23782  ptpjopn  23822  ptclsg  23825  ptcnp  23832  uffix2  24134  cnextf  24276  prdsxmslem2  24739  metustfbas  24767  metcld2  25519  dchrmusumlema  27710  dchrisum0lema  27731  elold  28105  lrrecfr  28189  istrkgld  28781  uvtx01vtx  29807  1loopgrvd2  29913  wspthsn  30266  iswspthn  30267  wspthsnon  30270  iswspthsnon  30274  wspthnon  30276  wlkiswwlks2  30293  wlkiswwlksupgr2  30295  wlklnwwlkln2lem  30300  wlksnwwlknvbij  30326  wspthsnwspthsnon  30334  elwwlks2on  30379  elwwlks2  30387  elwspths2spth  30388  clwlkclwwlk  30422  clwwlkvbij  30533  isgrpo  30922  adjeu  32314  iunrnmptss  32983  fcoinvbr  33023  2ndresdju  33067  fmptcof2  33075  acunirnmpt  33077  acunirnmpt2  33078  acunirnmpt2f  33079  aciunf1  33081  fnpreimac  33088  fpwrelmapffslem  33149  gsumwrd2dccatlem  33463  1arithidomlem1  33891  1arithidom  33893  fmcncfil  34387  bnj865  35378  bnj1388  35488  bnj1489  35511  fineqvrep  35586  fineqvac  35588  tz9.1regs  35606  satfrnmapom  35901  satf0op  35908  dmopab3rexdif  35936  prv1n  35962  rexxfr3dALT  36170  eldm3  36292  opelco3  36306  elsingles  36447  funpartlem  36473  dfrdg4  36482  linedegen  36674  prodeq12sdv  36789  cbvoprab2vw  36809  cbvoprab13vw  36812  cbvmodavw  36821  cbvopab1davw  36835  cbvopab2davw  36836  cbvoprab2davw  36843  cbvoprab12davw  36846  cbvoprab23davw  36847  cbvoprab13davw  36848  cbvsumdavw  36850  cbvproddavw  36851  cbvsumdavw2  36866  cbvproddavw2  36867  finminlem  36888  filnetlem4  36951  axtco1  37043  axtco1from2  37045  axtco1g  37046  dfttc4lem1  37098  dfttc4  37100  elttcirr  37101  ttcexg  37102  regsfromregtco  37108  mh-regprimbi  37115  mh-infprim1bi  37116  mobidvALT  37551  bj-issetwt  37569  bj-inex1gALT  37619  bj-axreprepsep  37771  bj-restuni  37798  bj-finsumval0  37988  csboprabg  38035  topdifinffinlem  38052  cbveud  38077  wl-sb8eut  38292  wl-sb8eutv  38293  sdclem1  38454  fdc  38456  ismgmOLD  38561  isriscg  38695  elrnres  38987  eldm4  38990  exan3  39009  exanres  39010  eldmcnv  39054  brxrn  39092  exeupre  39200  cosseq  39225  brcoss  39230  brcoss3  39232  eldm1cossres  39259  brcosscnv  39271  islshpat  39851  lshpsmreu  39943  isopos  40014  islpln5  40369  islvol5  40413  pmapjat1  40687  dibelval3  41981  diblsmopel  42005  mapdpglem3  42509  hdmapglem7a  42761  19.9dev  43046  fimgmcyc  43362  dfac11  43849  nnoeomeqom  44099  clcnvlem  44409  dfhe3  44561  ntrneineine0lem  44869  iotasbc  45189  iotasbc2  45190  brpermmodel  45772  permaxinf2lem  45781  permac8prim  45783  nregmodel  45786  fnchoice  45809  axccdom  45998  axccd  46004  stoweidlem35  46809  stoweidlem39  46813  dfatdmfcoafv2  48051  dfatco  48053  ichexmpl1  48278  ichnreuop  48281  ichreuopeq  48282  elsprel  48284  isgrim  48707  dfgric2  48740  gricushgr  48742  gricuspgr  48743  ushggricedg  48752  isubgrgrim  48754  uhgrimisgrgric  48756  grtri  48765  grtriprop  48766  isgrtri  48768  uspgrlim  48817  grlimedgclnbgr  48820  grlimgrtri  48828  dfgrlic2  48833  dfgrlic3  48835  grilcbri2  48836  map0cor  49692  nelsubc3lem  49907  thinccic  50308  istermc  50311  termcpropd  50340  discsntermlem  50407  basrestermcfolem  50408  discsnterm  50411  cnelsubclem  50440  bnd2d  50518