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  2894  eleq2w  2895  eleq1d  2896  eleq2dALT  2898  rexbidv2  3294  ceqsex2  3540  ceqsex2v  3541  alexeqg  3641  sbc2or  3777  sbc5  3796  sbcex2  3829  sbcabel  3855  elpreqprlem  4789  elpreqpr  4790  eluni  4834  csbuni  4860  intab  4899  cbvopab1  5132  cbvopab1g  5133  cbvopab1s  5135  axrep1  5184  axreplem  5185  zfrepclf  5191  axsepg  5197  zfauscl  5198  euotd  5396  opeliunxp  5612  brcog  5730  elrn2g  5754  dfdmf  5758  eldmg  5760  dmopabelb  5778  dmopab2rex  5779  dfrnf  5813  elrn2  5814  elrnmpt1  5823  brcodir  5972  dfco2a  6092  cores  6095  sbcfung  6372  brprcneu  6655  ssimaexg  6742  dmfco  6750  fndmdif  6805  fmptco  6884  fliftf  7061  cbvoprab1  7234  cbvoprab2  7235  uniuni  7477  dmtpos  7897  wrecseq123  7941  wfrlem1  7947  wfrlem3a  7950  wfrlem15  7962  rdglim2  8061  ecdmn0  8329  mapsnd  8443  bren  8511  brdomg  8512  domeng  8516  mapsnend  8581  isinf  8724  ac6sfi  8755  ordiso  8973  brwdom  9024  brwdom2  9030  zfregcl  9051  inf0  9077  zfinf  9095  bnd2  9315  isinffi  9414  acneq  9462  acni  9464  aceq0  9537  aceq3lem  9539  dfac3  9540  dfac5lem4  9545  dfac8  9554  dfac9  9555  kmlem1  9569  kmlem2  9570  kmlem8  9576  kmlem10  9578  kmlem13  9581  cfval  9662  cardcf  9667  cfeq0  9671  cfsuc  9672  cff1  9673  cflim3  9677  cofsmo  9684  isfin4  9712  axcc2lem  9851  axcc4dom  9856  domtriomlem  9857  dcomex  9862  axdc2lem  9863  axdc4lem  9870  zfac  9875  ac7g  9889  ac4c  9891  ac5  9892  ac6sg  9903  weth  9910  axrepndlem1  10007  axunndlem1  10010  zfcndrep  10029  zfcndinf  10033  zfcndac  10034  gruina  10233  grothomex  10244  genpass  10424  1idpr  10444  ltexprlem3  10453  ltexprlem4  10454  ltexpri  10458  reclem2pr  10463  reclem3pr  10464  recexpr  10466  infm3  11593  nnunb  11887  axdc4uz  13349  ishashinf  13818  relexpindlem  14417  sumeq1  15040  sumeq2w  15044  sumeq2ii  15045  summo  15069  fsum  15072  fsum2dlem  15120  ntrivcvgn0  15249  ntrivcvgmullem  15252  prodeq1f  15257  prodeq2w  15261  prodeq2ii  15262  prodmo  15285  zprod  15286  fprod  15290  fprodntriv  15291  fprod2dlem  15329  vdwapun  16305  vdwmc  16309  vdwmc2  16310  isacs  16917  dfiso2  17037  brssc  17079  isssc  17085  equivestrcsetc  17397  dirge  17842  gsumvalx  17881  gsumpropd  17883  gsumpropd2lem  17884  gsumress  17887  gsumval3eu  19019  gsumval3lem2  19021  dprd2d2  19161  znleval  20696  neitr  21783  cmpcovf  21994  hausmapdom  22103  ptval  22173  elpt  22175  ptpjopn  22215  ptclsg  22218  ptcnp  22225  uffix2  22527  cnextf  22669  prdsxmslem2  23134  metustfbas  23162  metcld2  23905  dchrmusumlema  26067  dchrisum0lema  26088  istrkgld  26243  uvtx01vtx  27177  1loopgrvd2  27283  wspthsn  27624  iswspthn  27625  wspthsnon  27628  iswspthsnon  27632  wspthnon  27634  wlkiswwlks2  27651  wlkiswwlksupgr2  27653  wlklnwwlkln2lem  27658  wlksnwwlknvbij  27685  wspthsnwspthsnon  27693  elwwlks2on  27736  elwwlks2  27743  elwspths2spth  27744  clwlkclwwlk  27778  clwwlkvbij  27890  isgrpo  28272  adjeu  29664  iunrnmptss  30317  fcoinvbr  30358  fmptcof2  30402  acunirnmpt  30404  acunirnmpt2  30405  acunirnmpt2f  30406  aciunf1  30408  fnpreimac  30416  fpwrelmapffslem  30468  fmcncfil  31195  bnj865  32216  bnj1388  32326  bnj1489  32349  satfrnmapom  32638  satf0op  32645  dmopab3rexdif  32673  prv1n  32699  eldm3  33018  opelco3  33039  frecseq123  33140  frrlem1  33144  frrlem13  33156  elsingles  33400  funpartlem  33424  dfrdg4  33433  linedegen  33625  finminlem  33687  filnetlem4  33750  mobidvALT  34202  bj-issetwt  34213  bj-restuni  34412  bj-finsumval0  34591  csbwrecsg  34632  csboprabg  34635  topdifinffinlem  34652  cbveud  34677  wl-sb8eut  34848  wl-dfrmof  34890  sdclem1  35051  fdc  35053  ismgmOLD  35161  isriscg  35295  eldm4  35564  exan3  35584  exanres  35585  eldmcnv  35635  brxrn  35659  cosseq  35704  brcoss  35709  brcoss3  35711  eldm1cossres  35733  brcosscnv  35745  islshpat  36186  lshpsmreu  36278  isopos  36349  islpln5  36704  islvol5  36748  pmapjat1  37022  dibelval3  38316  diblsmopel  38340  mapdpglem3  38844  hdmapglem7a  39096  dfac11  39738  clcnvlem  40057  dfhe3  40195  ntrneineine0lem  40507  iotasbc  40825  iotasbc2  40826  fnchoice  41360  axccdom  41561  axccd  41569  stoweidlem35  42394  stoweidlem39  42398  dfatdmfcoafv2  43527  dfatco  43529  ichexmpl1  43705  ichnreuop  43708  ichreuopeq  43709  elsprel  43711  isomgr  44062  isomgreqve  44064  isomushgr  44065  isomuspgr  44073  isomgrsym  44075  isomgrtr  44078  ushrisomgr  44080  opeliun2xp  44455  bnd2d  44858