Theorem exbidv 1837

Description: Formula-building rule for existential quantifier (deduction rule). (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 1827	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1781	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 195  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  2exbidv  1839  3exbidv  1840  eubid  2476  eleq1d  2672  eleq2dALT  2675  rexbidv2  3030  ceqsex2  3217  alexeqg  3302  sbc2or  3411  sbc5  3427  sbcex2  3453  sbcabel  3483  elpreqprlem  4333  elpreqpr  4334  eluni  4375  csbuni  4402  intab  4442  cbvopab1  4655  cbvopab1s  4657  axrep1  4700  axrep2  4701  axrep3  4702  zfrepclf  4705  axsep2  4710  zfauscl  4711  euotd  4900  opeliunxp  5093  brcog  5210  elrn2g  5235  dfdmf  5239  eldmg  5241  dfrnf  5285  elrn2  5286  elrnmpt1  5295  brcodir  5434  dfco2a  5552  cores  5555  sbcfung  5827  brprcneu  6096  ssimaexg  6174  dmfco  6182  fndmdif  6229  fmptco  6303  fliftf  6465  cbvoprab1  6625  cbvoprab2  6626  snnex  6862  uniuni  6865  dmtpos  7251  wrecseq123  7295  wfrlem1  7301  wfrlem3a  7304  wfrlem15  7316  rdglim2  7415  ecdmn0  7676  mapsn  7785  bren  7850  brdomg  7851  domeng  7855  isinf  8058  ac6sfi  8089  ordiso  8304  brwdom  8355  brwdom2  8361  zfregcl  8382  zfregclOLD  8384  inf0  8401  zfinf  8419  bnd2  8639  isinffi  8701  acneq  8749  acni  8751  aceq0  8824  aceq3lem  8826  dfac3  8827  dfac5lem4  8832  dfac8  8840  dfac9  8841  kmlem1  8855  kmlem2  8856  kmlem8  8862  kmlem10  8864  kmlem13  8867  cfval  8952  cardcf  8957  cfeq0  8961  cfsuc  8962  cff1  8963  cflim3  8967  cofsmo  8974  isfin4  9002  axcc2lem  9141  axcc4dom  9146  domtriomlem  9147  dcomex  9152  axdc2lem  9153  axdc4lem  9160  zfac  9165  ac7g  9179  ac4c  9181  ac5  9182  ac6sg  9193  weth  9200  axrepndlem1  9293  axunndlem1  9296  zfcndrep  9315  zfcndinf  9319  zfcndac  9320  gruina  9519  grothomex  9530  genpass  9710  1idpr  9730  ltexprlem3  9739  ltexprlem4  9740  ltexpri  9744  reclem2pr  9749  reclem3pr  9750  recexpr  9752  infm3  10861  nnunb  11165  axdc4uz  12645  ishashinf  13104  relexpindlem  13651  sumeq1  14267  sumeq2w  14270  sumeq2ii  14271  summo  14295  fsum  14298  fsum2dlem  14343  ntrivcvgn0  14469  ntrivcvgmullem  14472  prodeq1f  14477  prodeq2w  14481  prodeq2ii  14482  prodmo  14505  zprod  14506  fprod  14510  fprodntriv  14511  fprod2dlem  14549  ncoprmgcdne1b  15201  vdwapun  15516  vdwmc  15520  vdwmc2  15521  isacs  16135  dfiso2  16255  brssc  16297  isssc  16303  equivestrcsetc  16615  dirge  17060  gsumvalx  17093  gsumpropd  17095  gsumpropd2lem  17096  gsumress  17099  gsumval3eu  18128  gsumval3lem2  18130  dprd2d2  18266  znleval  19722  neitr  20794  cmpcovf  21004  hausmapdom  21113  ptval  21183  elpt  21185  ptpjopn  21225  ptclsg  21228  ptcnp  21235  uffix2  21538  cnextf  21680  prdsxmslem2  22144  metustfbas  22172  metcld2  22913  dchrmusumlema  24982  dchrisum0lema  25003  istrkgld  25158  uvtx01vtx  26020  wlkiswwlk2  26225  wlklniswwlkn2  26228  wlknwwlknvbij  26268  clwlkisclwwlk  26317  clwwlkvbij  26329  isgrpo  26735  adjeu  28132  fcoinvbr  28799  fmptcof2  28839  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  aciunf1  28845  fpwrelmapffslem  28895  fmcncfil  29305  bnj865  30247  bnj1388  30355  bnj1489  30378  eldm3  30905  opelco3  30923  frrlem1  31024  elsingles  31195  funpartlem  31219  dfrdg4  31228  linedegen  31420  finminlem  31482  filnetlem4  31546  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-eleq1w  32040  bj-eleq2w  32041  bj-issetwt  32053  bj-ax8  32080  bj-axsep2  32113  bj-restuni  32231  bj-finsumval0  32324  csbwrecsg  32349  csboprabg  32352  topdifinffinlem  32371  wl-sb8eut  32538  sdclem1  32709  fdc  32711  ismgmOLD  32819  isriscg  32953  islshpat  33322  lshpsmreu  33414  isopos  33485  islpln5  33839  islvol5  33883  pmapjat1  34157  dibelval3  35454  diblsmopel  35478  mapdpglem3  35982  hdmapglem7a  36237  dfac11  36650  clcnvlem  36949  dfhe3  37089  ntrneineine0lem  37401  iotasbc  37642  iotasbc2  37643  sbcexgOLD  37774  csbunigOLD  38073  csbxpgOLD  38075  csbrngOLD  38078  fnchoice  38211  mapsnd  38383  mapsnend  38386  axccdom  38411  axccd  38424  stoweidlem35  38928  stoweidlem39  38932  uvtxa01vtx0  40623  1loopgrvd2  40718  wspthsn  41046  iswspthn  41047  wspthsnon  41050  iswspthsnon  41052  wspthnon  41054  1wlkiswwlks2  41072  1wlkiswwlksupgr2  41074  1wlklnwwlkln2lem  41079  wlksnwwlknvbij  41114  wspthsnwspthsnon  41122  elwwlks2on  41162  elwwlks2  41170  elwspths2spth  41171  clwlkclwwlk  41211  clwwlksvbij  41229  opeliun2xp  41904  bnd2d  42226