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 208  ∃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 209  df-ex 1780

This theorem is referenced by:  nfbidv  1922  2exbidv  1924  3exbidv  1925  eleq1w  2898  eleq2w  2899  eleq1d  2900  eleq2dALT  2902  rexbidv2  3298  ceqsex2  3546  ceqsex2v  3547  alexeqg  3647  sbc2or  3784  sbc5  3803  sbcex2  3837  sbcabel  3864  elpreqprlem  4799  elpreqpr  4800  eluni  4844  csbuni  4870  intab  4909  cbvopab1  5142  cbvopab1g  5143  cbvopab1s  5145  axrep1  5194  axreplem  5195  zfrepclf  5201  axsepg  5207  zfauscl  5208  euotd  5406  opeliunxp  5622  brcog  5740  elrn2g  5764  dfdmf  5768  eldmg  5770  dmopabelb  5788  dmopab2rex  5789  dfrnf  5823  elrn2  5824  elrnmpt1  5833  brcodir  5982  dfco2a  6102  cores  6105  sbcfung  6382  brprcneu  6665  ssimaexg  6752  dmfco  6760  fndmdif  6815  fmptco  6894  fliftf  7071  cbvoprab1  7244  cbvoprab2  7245  uniuni  7487  dmtpos  7907  wrecseq123  7951  wfrlem1  7957  wfrlem3a  7960  wfrlem15  7972  rdglim2  8071  ecdmn0  8339  mapsnd  8453  bren  8521  brdomg  8522  domeng  8526  mapsnend  8591  isinf  8734  ac6sfi  8765  ordiso  8983  brwdom  9034  brwdom2  9040  zfregcl  9061  inf0  9087  zfinf  9105  bnd2  9325  isinffi  9424  acneq  9472  acni  9474  aceq0  9547  aceq3lem  9549  dfac3  9550  dfac5lem4  9555  dfac8  9564  dfac9  9565  kmlem1  9579  kmlem2  9580  kmlem8  9586  kmlem10  9588  kmlem13  9591  cfval  9672  cardcf  9677  cfeq0  9681  cfsuc  9682  cff1  9683  cflim3  9687  cofsmo  9694  isfin4  9722  axcc2lem  9861  axcc4dom  9866  domtriomlem  9867  dcomex  9872  axdc2lem  9873  axdc4lem  9880  zfac  9885  ac7g  9899  ac4c  9901  ac5  9902  ac6sg  9913  weth  9920  axrepndlem1  10017  axunndlem1  10020  zfcndrep  10039  zfcndinf  10043  zfcndac  10044  gruina  10243  grothomex  10254  genpass  10434  1idpr  10454  ltexprlem3  10463  ltexprlem4  10464  ltexpri  10468  reclem2pr  10473  reclem3pr  10474  recexpr  10476  infm3  11603  nnunb  11896  axdc4uz  13355  ishashinf  13824  relexpindlem  14425  sumeq1  15048  sumeq2w  15052  sumeq2ii  15053  summo  15077  fsum  15080  fsum2dlem  15128  ntrivcvgn0  15257  ntrivcvgmullem  15260  prodeq1f  15265  prodeq2w  15269  prodeq2ii  15270  prodmo  15293  zprod  15294  fprod  15298  fprodntriv  15299  fprod2dlem  15337  vdwapun  16313  vdwmc  16317  vdwmc2  16318  isacs  16925  dfiso2  17045  brssc  17087  isssc  17093  equivestrcsetc  17405  dirge  17850  gsumvalx  17889  gsumpropd  17891  gsumpropd2lem  17892  gsumress  17895  gsumval3eu  19027  gsumval3lem2  19029  dprd2d2  19169  znleval  20704  neitr  21791  cmpcovf  22002  hausmapdom  22111  ptval  22181  elpt  22183  ptpjopn  22223  ptclsg  22226  ptcnp  22233  uffix2  22535  cnextf  22677  prdsxmslem2  23142  metustfbas  23170  metcld2  23913  dchrmusumlema  26072  dchrisum0lema  26093  istrkgld  26248  uvtx01vtx  27182  1loopgrvd2  27288  wspthsn  27629  iswspthn  27630  wspthsnon  27633  iswspthsnon  27637  wspthnon  27639  wlkiswwlks2  27656  wlkiswwlksupgr2  27658  wlklnwwlkln2lem  27663  wlksnwwlknvbij  27690  wspthsnwspthsnon  27698  elwwlks2on  27741  elwwlks2  27748  elwspths2spth  27749  clwlkclwwlk  27783  clwwlkvbij  27895  isgrpo  28277  adjeu  29669  iunrnmptss  30320  fcoinvbr  30361  fmptcof2  30405  acunirnmpt  30407  acunirnmpt2  30408  acunirnmpt2f  30409  aciunf1  30411  fnpreimac  30419  fpwrelmapffslem  30471  fmcncfil  31178  bnj865  32199  bnj1388  32309  bnj1489  32332  satfrnmapom  32621  satf0op  32628  dmopab3rexdif  32656  prv1n  32682  eldm3  33001  opelco3  33022  frecseq123  33123  frrlem1  33127  frrlem13  33139  elsingles  33383  funpartlem  33407  dfrdg4  33416  linedegen  33608  finminlem  33670  filnetlem4  33733  mobidvALT  34185  bj-issetwt  34193  bj-restuni  34392  bj-finsumval0  34571  csbwrecsg  34612  csboprabg  34615  topdifinffinlem  34632  cbveud  34657  wl-sb8eut  34817  wl-dfrmof  34859  sdclem1  35022  fdc  35024  ismgmOLD  35132  isriscg  35266  eldm4  35535  exan3  35555  exanres  35556  eldmcnv  35606  brxrn  35630  cosseq  35675  brcoss  35680  brcoss3  35682  eldm1cossres  35704  brcosscnv  35716  islshpat  36157  lshpsmreu  36249  isopos  36320  islpln5  36675  islvol5  36719  pmapjat1  36993  dibelval3  38287  diblsmopel  38311  mapdpglem3  38815  hdmapglem7a  39067  dfac11  39668  clcnvlem  39989  dfhe3  40127  ntrneineine0lem  40439  iotasbc  40757  iotasbc2  40758  fnchoice  41292  axccdom  41493  axccd  41501  stoweidlem35  42327  stoweidlem39  42331  dfatdmfcoafv2  43460  dfatco  43462  ichexmpl1  43638  ichnreuop  43641  ichreuopeq  43642  elsprel  43644  isomgr  43995  isomgreqve  43997  isomushgr  43998  isomuspgr  44006  isomgrsym  44008  isomgrtr  44011  ushrisomgr  44013  opeliun2xp  44388  bnd2d  44791