Theorem exbidv 1954

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1900 and exbid 2260. (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  2844  eleq2w  2845  eleq1d  2846  eleq2dALT  2848  clelab  2905  rexbidv2  3183  rmoeq1  3397  ceqsex2  3501  ceqsex2v  3502  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  5244  axsepg  5250  sepg  5251  zfausclOLD  5253  sels  5408  euotd  5486  opeliunxp  5718  opeliun2xp  5719  brcog  5844  elrn2g  5872  dfdmf  5878  eldmg  5880  dmun  5892  dmopabelb  5898  dmopab2rex  5899  dm0rn0  5906  dfrnf  5932  elrnmpt1  5942  dfrn7  6066  brcodir  6113  dfco2a  6247  cores  6250  sbcfungOLD  6564  brprcneu  6875  brprcneuALT  6876  ssimaexg  6971  dmfco  6981  fndmdif  7041  fmptco  7130  fliftf  7323  oprabbidv  7486  cbvoprab1  7507  cbvoprab2  7508  cbvoprab12v  7510  imaeqexov  7659  uniuni  7776  dmtpos  8255  frecseq123  8300  csbfrecsg  8302  frrlem1  8304  frrlem13  8316  rdglim2  8440  ecdmn0  8770  mapsnd  8914  breng  8982  brdom2g  8984  domeng  8989  mapsnend  9064  isinf  9256  ac6sfi  9275  ordiso  9510  brwdom  9561  brwdom2  9567  zfregcl  9588  zfregclOLD  9589  inf0  9622  zfinf  9640  ttrcleq  9710  brttrcl  9714  brttrcl2  9715  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  ttrclselem2  9727  bnd2  9956  bnd2d  9968  isinffi  10073  acneq  10122  acni  10124  aceq0  10197  aceq3lem  10199  dfac3  10200  dfac5lem4  10205  dfac8  10214  dfac9  10215  kmlem1  10229  kmlem2  10230  kmlem8  10236  kmlem10  10238  kmlem13  10241  cfval  10324  cardcf  10329  cfeq0  10334  cfsuc  10335  cff1  10336  cflim3  10340  cofsmo  10347  isfin4  10375  axcc2lem  10514  axcc4dom  10519  domtriomlem  10520  dcomex  10525  axdc2lem  10526  axdc4lem  10533  zfac  10538  ac7g  10552  ac4c  10554  ac5  10555  ac6sg  10566  weth  10573  axrepndlem1  10677  axunndlem1  10680  zfcndrep  10699  zfcndinf  10703  zfcndac  10704  gruina  10903  grothomex  10914  genpass  11094  1idpr  11114  ltexprlem3  11123  ltexprlem4  11124  ltexpri  11128  reclem2pr  11133  reclem3pr  11134  recexpr  11136  infm3  12276  nnunb  12602  axdc4uz  14127  ishashinf  14608  relexpindlem  15216  sumeq1  15856  sumeq2w  15859  sumeq2ii  15860  sumeq2sdv  15870  summo  15883  fsum  15886  fsum2dlem  15936  ntrivcvgn0  16067  ntrivcvgmullem  16070  prodeq1f  16075  prodeq1  16076  prodeq2w  16079  prodeq2ii  16080  prodeq2sdv  16091  prodmo  16103  zprod  16104  fprod  16108  fprodntriv  16109  fprod2dlem  16147  vdwapun  17152  vdwmc  17156  vdwmc2  17157  isacs  17825  dfiso2  17947  brssc  17989  isssc  17995  equivestrcsetc  18326  dirge  18777  gsumvalx  18865  gsumpropd  18867  gsumpropd2lem  18868  gsumress  18871  degenmgm2nfun  19139  gsumval3eu  20118  gsumval3lem2  20120  dprd2d2  20260  znleval  21860  neitr  23498  cmpcovf  23709  hausmapdom  23819  ptval  23889  elpt  23891  ptpjopn  23931  ptclsg  23934  ptcnp  23941  uffix2  24243  cnextf  24385  prdsxmslem2  24848  metustfbas  24876  metcld2  25628  dchrmusumlema  27820  dchrisum0lema  27841  elold  28245  lrrecfr  28329  istrkgld  28921  uvtx01vtx  29978  1loopgrvd2  30084  wspthsn  30437  iswspthn  30438  wspthsnon  30441  iswspthsnon  30445  wspthnon  30447  wlkiswwlks2  30464  wlkiswwlksupgr2  30466  wlklnwwlkln2lem  30471  wlksnwwlknvbij  30497  wspthsnwspthsnon  30505  elwwlks2on  30550  elwwlks2  30558  elwspths2spth  30559  clwlkclwwlk  30593  clwwlkvbij  30704  isgrpo  31099  adjeu  32491  iunrnmptss  33159  fcoinvbr  33199  2ndresdju  33243  fmptcof2  33251  acunirnmpt  33253  acunirnmpt2  33254  acunirnmpt2f  33255  aciunf1  33257  fnpreimac  33264  fpwrelmapffslem  33324  gsumwrd2dccatlem  33638  1arithidomlem1  34067  1arithidom  34069  fmcncfil  34563  bnj865  35553  bnj1388  35663  bnj1489  35686  acwer1prclem  35759  fineqvrep  35782  fineqvac  35784  tz9.1regs  35802  onprcf1acwevdlem1  35895  satfrnmapom  36135  satf0op  36142  dmopab3rexdif  36170  prv1n  36196  rexxfr3dALT  36404  eldm3  36526  opelco3  36539  elsingles  36680  funpartlem  36706  dfrdg4  36715  linedegen  36908  prodeq12sdv  37007  cbvoprab2vw  37027  cbvoprab13vw  37030  cbvmodavw  37039  cbvopab1davw  37053  cbvopab2davw  37054  cbvoprab2davw  37061  cbvoprab12davw  37064  cbvoprab23davw  37065  cbvoprab13davw  37066  cbvsumdavw  37068  cbvproddavw  37069  cbvsumdavw2  37084  cbvproddavw2  37085  finminlem  37106  filnetlem4  37169  axtco1  37261  axtco1from2  37263  axtco1g  37264  dfttc4lem1  37316  dfttc4  37318  elttcirr  37319  ttcexg  37320  regsfromregtco  37326  mh-regprimbi  37333  mh-infprim1bi  37334  mobidvALT  37769  bj-issetwt  37787  bj-inex1gALT  37837  bj-axreprepsep  37991  bj-restuni  38018  bj-finsumval0  38206  csboprabg  38253  topdifinffinlem  38270  cbveud  38295  wl-sb8eut  38510  wl-sb8eutv  38511  sdclem1  38677  fdc  38679  ismgmOLD  38784  isriscg  38918  elrnres  39210  eldm4  39213  exan3  39232  exanres  39233  eldmcnv  39277  brxrn  39315  exeupre  39423  cosseq  39448  brcoss  39453  brcoss3  39455  eldm1cossres  39482  brcosscnv  39494  islshpat  40074  lshpsmreu  40166  isopos  40237  islpln5  40592  islvol5  40636  pmapjat1  40910  dibelval3  42204  diblsmopel  42228  mapdpglem3  42732  hdmapglem7a  42984  19.9dev  43269  fimgmcyc  43598  dfac11  44063  nnoeomeqom  44313  clcnvlem  44622  dfhe3  44774  ntrneineine0lem  45082  iotasbc  45402  iotasbc2  45403  brpermmodel  45992  permaxinf2lem  46001  permac8prim  46003  nregmodel  46006  fnchoice  46045  axccdom  46234  axccd  46240  stoweidlem35  47044  stoweidlem39  47048  dfatdmfcoafv2  48323  dfatco  48325  ichexmpl1  48550  ichnreuop  48553  ichreuopeq  48554  elsprel  48556  isgrim  48979  dfgric2  49012  gricushgr  49014  gricuspgr  49015  ushggricedg  49024  isubgrgrim  49026  uhgrimisgrgric  49028  grtri  49037  grtriprop  49038  isgrtri  49040  uspgrlim  49089  grlimedgclnbgr  49092  grlimgrtri  49100  dfgrlic2  49105  dfgrlic3  49107  grilcbri2  49108  map0cor  49964  nelsubc3lem  50177  thinccic  50578  istermc  50581  termcpropd  50610  discsntermlem  50677  basrestermcfolem  50678  discsnterm  50681  cnelsubclem  50710