Theorem exbidv 1954

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1900 and exbid 2259. (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  2843  eleq2w  2844  eleq1d  2845  eleq2dALT  2847  clelab  2904  rexbidv2  3182  rmoeq1  3396  ceqsex2  3500  ceqsex2v  3501  alexeqg  3605  sbc2or  3748  sbc5ALT  3768  sbcex2  3799  sbcabel  3825  elpreqprlem  4826  elpreqpr  4827  eluni  4870  csbuni  4898  intab  4938  cbvopab1  5179  cbvopab1g  5180  cbvopab1s  5182  cbvopab1v  5183  axrep1  5233  axreplem  5234  zfrepclf  5246  axsepg  5252  sepg  5253  zfausclOLD  5255  sels  5415  euotd  5490  opeliunxp  5722  opeliun2xp  5723  brcog  5846  elrn2g  5874  dfdmf  5880  eldmg  5882  dmun  5894  dmopabelb  5900  dmopab2rex  5901  dm0rn0  5908  dfrnf  5934  elrnmpt1  5944  brcodir  6113  dfco2a  6242  cores  6245  sbcfungOLD  6558  brprcneu  6869  brprcneuALT  6870  ssimaexg  6965  dmfco  6975  fndmdif  7035  fmptco  7124  fliftf  7317  oprabbidv  7480  cbvoprab1  7501  cbvoprab2  7502  cbvoprab12v  7504  imaeqexov  7653  uniuni  7762  dmtpos  8237  frecseq123  8282  csbfrecsg  8284  frrlem1  8286  frrlem13  8298  rdglim2  8422  ecdmn0  8750  mapsnd  8894  breng  8962  brdom2g  8964  domeng  8969  mapsnend  9044  isinf  9236  ac6sfi  9255  ordiso  9489  brwdom  9540  brwdom2  9546  zfregcl  9567  zfregclOLD  9568  inf0  9601  zfinf  9619  ttrcleq  9689  brttrcl  9693  brttrcl2  9694  ssttrcl  9695  ttrcltr  9696  ttrclss  9700  ttrclselem2  9706  bnd2  9896  isinffi  9998  acneq  10047  acni  10049  aceq0  10122  aceq3lem  10124  dfac3  10125  dfac5lem4  10130  dfac8  10139  dfac9  10140  kmlem1  10154  kmlem2  10155  kmlem8  10161  kmlem10  10163  kmlem13  10166  cfval  10249  cardcf  10254  cfeq0  10259  cfsuc  10260  cff1  10261  cflim3  10265  cofsmo  10272  isfin4  10300  axcc2lem  10439  axcc4dom  10444  domtriomlem  10445  dcomex  10450  axdc2lem  10451  axdc4lem  10458  zfac  10463  ac7g  10477  ac4c  10479  ac5  10480  ac6sg  10491  weth  10498  axrepndlem1  10602  axunndlem1  10605  zfcndrep  10624  zfcndinf  10628  zfcndac  10629  gruina  10828  grothomex  10839  genpass  11019  1idpr  11039  ltexprlem3  11048  ltexprlem4  11049  ltexpri  11053  reclem2pr  11058  reclem3pr  11059  recexpr  11061  infm3  12199  nnunb  12525  axdc4uz  14049  ishashinf  14529  relexpindlem  15137  sumeq1  15777  sumeq2w  15780  sumeq2ii  15781  sumeq2sdv  15791  summo  15804  fsum  15807  fsum2dlem  15857  ntrivcvgn0  15988  ntrivcvgmullem  15991  prodeq1f  15996  prodeq1  15997  prodeq2w  16000  prodeq2ii  16001  prodeq2sdv  16012  prodmo  16024  zprod  16025  fprod  16029  fprodntriv  16030  fprod2dlem  16068  vdwapun  17067  vdwmc  17071  vdwmc2  17072  isacs  17740  dfiso2  17862  brssc  17904  isssc  17910  equivestrcsetc  18241  dirge  18692  gsumvalx  18779  gsumpropd  18781  gsumpropd2lem  18782  gsumress  18785  degenmgm2nfun  19053  gsumval3eu  20032  gsumval3lem2  20034  dprd2d2  20174  znleval  21768  neitr  23406  cmpcovf  23617  hausmapdom  23727  ptval  23797  elpt  23799  ptpjopn  23839  ptclsg  23842  ptcnp  23849  uffix2  24151  cnextf  24293  prdsxmslem2  24756  metustfbas  24784  metcld2  25536  dchrmusumlema  27730  dchrisum0lema  27751  elold  28125  lrrecfr  28209  istrkgld  28801  uvtx01vtx  29858  1loopgrvd2  29964  wspthsn  30317  iswspthn  30318  wspthsnon  30321  iswspthsnon  30325  wspthnon  30327  wlkiswwlks2  30344  wlkiswwlksupgr2  30346  wlklnwwlkln2lem  30351  wlksnwwlknvbij  30377  wspthsnwspthsnon  30385  elwwlks2on  30430  elwwlks2  30438  elwspths2spth  30439  clwlkclwwlk  30473  clwwlkvbij  30584  isgrpo  30979  adjeu  32371  iunrnmptss  33039  fcoinvbr  33079  2ndresdju  33123  fmptcof2  33131  acunirnmpt  33133  acunirnmpt2  33134  acunirnmpt2f  33135  aciunf1  33137  fnpreimac  33144  fpwrelmapffslem  33204  gsumwrd2dccatlem  33518  1arithidomlem1  33946  1arithidom  33948  fmcncfil  34442  bnj865  35433  bnj1388  35543  bnj1489  35566  fineqvrep  35641  fineqvac  35643  tz9.1regs  35661  satfrnmapom  35950  satf0op  35957  dmopab3rexdif  35985  prv1n  36011  rexxfr3dALT  36219  eldm3  36341  opelco3  36355  elsingles  36496  funpartlem  36522  dfrdg4  36531  linedegen  36724  prodeq12sdv  36839  cbvoprab2vw  36859  cbvoprab13vw  36862  cbvmodavw  36871  cbvopab1davw  36885  cbvopab2davw  36886  cbvoprab2davw  36893  cbvoprab12davw  36896  cbvoprab23davw  36897  cbvoprab13davw  36898  cbvsumdavw  36900  cbvproddavw  36901  cbvsumdavw2  36916  cbvproddavw2  36917  finminlem  36938  filnetlem4  37001  axtco1  37093  axtco1from2  37095  axtco1g  37096  dfttc4lem1  37148  dfttc4  37150  elttcirr  37151  ttcexg  37152  regsfromregtco  37158  mh-regprimbi  37165  mh-infprim1bi  37166  mobidvALT  37601  bj-issetwt  37619  bj-inex1gALT  37669  bj-axreprepsep  37821  bj-restuni  37848  bj-finsumval0  38038  csboprabg  38085  topdifinffinlem  38102  cbveud  38127  wl-sb8eut  38342  wl-sb8eutv  38343  sdclem1  38494  fdc  38496  ismgmOLD  38601  isriscg  38735  elrnres  39027  eldm4  39030  exan3  39049  exanres  39050  eldmcnv  39094  brxrn  39132  exeupre  39240  cosseq  39265  brcoss  39270  brcoss3  39272  eldm1cossres  39299  brcosscnv  39311  islshpat  39891  lshpsmreu  39983  isopos  40054  islpln5  40409  islvol5  40453  pmapjat1  40727  dibelval3  42021  diblsmopel  42045  mapdpglem3  42549  hdmapglem7a  42801  19.9dev  43086  fimgmcyc  43417  dfac11  43904  nnoeomeqom  44154  clcnvlem  44464  dfhe3  44616  ntrneineine0lem  44924  iotasbc  45244  iotasbc2  45245  brpermmodel  45827  permaxinf2lem  45836  permac8prim  45838  nregmodel  45841  fnchoice  45864  axccdom  46053  axccd  46059  stoweidlem35  46864  stoweidlem39  46868  dfatdmfcoafv2  48143  dfatco  48145  ichexmpl1  48370  ichnreuop  48373  ichreuopeq  48374  elsprel  48376  isgrim  48799  dfgric2  48832  gricushgr  48834  gricuspgr  48835  ushggricedg  48844  isubgrgrim  48846  uhgrimisgrgric  48848  grtri  48857  grtriprop  48858  isgrtri  48860  uspgrlim  48909  grlimedgclnbgr  48912  grlimgrtri  48920  dfgrlic2  48925  dfgrlic3  48927  grilcbri2  48928  map0cor  49784  nelsubc3lem  49997  thinccic  50398  istermc  50401  termcpropd  50430  discsntermlem  50497  basrestermcfolem  50498  discsnterm  50501  cnelsubclem  50530  bnd2d  50608