Theorem exbidv 1925

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1871 and exbid 2217. (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 1914	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1871	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  nfbidv  1926  2exbidv  1928  3exbidv  1929  eleq1w  2822  eleq2w  2823  eleq1d  2824  eleq2dALT  2826  clelab  2884  nfcriOLD  2898  rexbidv2  3225  cgsex4g  3477  ceqsex2  3483  ceqsex2v  3484  alexeqg  3582  sbc2or  3726  sbc5ALT  3746  sbcex2  3782  sbcabel  3812  elpreqprlem  4797  elpreqpr  4798  eluni  4843  csbuni  4871  intab  4910  cbvopab1  5150  cbvopab1g  5151  cbvopab1s  5153  cbvopab1v  5154  axrep1  5211  axreplem  5212  zfrepclf  5219  axsepg  5225  zfauscl  5226  euotd  5428  opeliunxp  5655  brcog  5778  elrn2g  5802  dfdmf  5808  eldmg  5810  dmopabelb  5828  dmopab2rex  5829  dfrnf  5862  elrnmpt1  5870  brcodir  6029  dfco2a  6154  cores  6157  sbcfung  6465  brprcneu  6773  brprcneuALT  6774  ssimaexg  6863  dmfco  6873  fndmdif  6928  fmptco  7010  fliftf  7195  oprabbidv  7350  cbvoprab1  7371  cbvoprab2  7372  uniuni  7621  dmtpos  8063  frecseq123  8107  csbfrecsg  8109  frrlem1  8111  frrlem13  8123  wrecseq123OLD  8140  wfrlem1OLD  8148  wfrlem3OLDa  8151  wfrlem15OLD  8163  rdglim2  8272  ecdmn0  8554  mapsnd  8683  breng  8751  brenOLD  8753  brdom2g  8754  brdomgOLD  8756  domeng  8761  mapsnend  8835  isinf  9045  ac6sfi  9067  ordiso  9284  brwdom  9335  brwdom2  9341  zfregcl  9362  inf0  9388  zfinf  9406  ttrcleq  9476  brttrcl  9480  brttrcl2  9481  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  bnd2  9660  isinffi  9759  acneq  9808  acni  9810  aceq0  9883  aceq3lem  9885  dfac3  9886  dfac5lem4  9891  dfac8  9900  dfac9  9901  kmlem1  9915  kmlem2  9916  kmlem8  9922  kmlem10  9924  kmlem13  9927  cfval  10012  cardcf  10017  cfeq0  10021  cfsuc  10022  cff1  10023  cflim3  10027  cofsmo  10034  isfin4  10062  axcc2lem  10201  axcc4dom  10206  domtriomlem  10207  dcomex  10212  axdc2lem  10213  axdc4lem  10220  zfac  10225  ac7g  10239  ac4c  10241  ac5  10242  ac6sg  10253  weth  10260  axrepndlem1  10357  axunndlem1  10360  zfcndrep  10379  zfcndinf  10383  zfcndac  10384  gruina  10583  grothomex  10594  genpass  10774  1idpr  10794  ltexprlem3  10803  ltexprlem4  10804  ltexpri  10808  reclem2pr  10813  reclem3pr  10814  recexpr  10816  infm3  11943  nnunb  12238  axdc4uz  13713  ishashinf  14186  relexpindlem  14783  sumeq1  15409  sumeq2w  15413  sumeq2ii  15414  summo  15438  fsum  15441  fsum2dlem  15491  ntrivcvgn0  15619  ntrivcvgmullem  15622  prodeq1f  15627  prodeq2w  15631  prodeq2ii  15632  prodmo  15655  zprod  15656  fprod  15660  fprodntriv  15661  fprod2dlem  15699  vdwapun  16684  vdwmc  16688  vdwmc2  16689  isacs  17369  dfiso2  17493  brssc  17535  isssc  17541  equivestrcsetc  17878  dirge  18330  gsumvalx  18369  gsumpropd  18371  gsumpropd2lem  18372  gsumress  18375  gsumval3eu  19514  gsumval3lem2  19516  dprd2d2  19656  znleval  20771  neitr  22340  cmpcovf  22551  hausmapdom  22660  ptval  22730  elpt  22732  ptpjopn  22772  ptclsg  22775  ptcnp  22782  uffix2  23084  cnextf  23226  prdsxmslem2  23694  metustfbas  23722  metcld2  24480  dchrmusumlema  26650  dchrisum0lema  26671  istrkgld  26829  uvtx01vtx  27773  1loopgrvd2  27879  wspthsn  28222  iswspthn  28223  wspthsnon  28226  iswspthsnon  28230  wspthnon  28232  wlkiswwlks2  28249  wlkiswwlksupgr2  28251  wlklnwwlkln2lem  28256  wlksnwwlknvbij  28282  wspthsnwspthsnon  28290  elwwlks2on  28333  elwwlks2  28340  elwspths2spth  28341  clwlkclwwlk  28375  clwwlkvbij  28486  isgrpo  28868  adjeu  30260  iunrnmptss  30914  fcoinvbr  30956  2ndresdju  30995  fmptcof2  31003  acunirnmpt  31005  acunirnmpt2  31006  acunirnmpt2f  31007  aciunf1  31009  fnpreimac  31017  fpwrelmapffslem  31076  fmcncfil  31890  bnj865  32912  bnj1388  33022  bnj1489  33045  fineqvrep  33073  fineqvac  33075  satfrnmapom  33341  satf0op  33348  dmopab3rexdif  33376  prv1n  33402  imaeqsexv  33699  eldm3  33737  opelco3  33758  elold  34062  lrrecfr  34109  elsingles  34229  funpartlem  34253  dfrdg4  34262  linedegen  34454  finminlem  34516  filnetlem4  34579  mobidvALT  35050  bj-issetwt  35068  bj-restuni  35277  bj-finsumval0  35465  csboprabg  35510  topdifinffinlem  35527  cbveud  35552  wl-sb8eut  35741  sdclem1  35910  fdc  35912  ismgmOLD  36017  isriscg  36151  eldm4  36417  exan3  36437  exanres  36438  eldmcnv  36487  brxrn  36511  cosseq  36556  brcoss  36561  brcoss3  36563  eldm1cossres  36585  brcosscnv  36597  islshpat  37038  lshpsmreu  37130  isopos  37201  islpln5  37556  islvol5  37600  pmapjat1  37874  dibelval3  39168  diblsmopel  39192  mapdpglem3  39696  hdmapglem7a  39948  19.9dev  40185  dfac11  40894  clcnvlem  41238  dfhe3  41390  ntrneineine0lem  41700  iotasbc  42044  iotasbc2  42045  fnchoice  42579  axccdom  42769  axccd  42775  stoweidlem35  43583  stoweidlem39  43587  dfatdmfcoafv2  44757  dfatco  44759  ichexmpl1  44932  ichnreuop  44935  ichreuopeq  44936  elsprel  44938  isomgr  45286  isomgreqve  45288  isomushgr  45289  isomuspgr  45297  isomgrsym  45299  isomgrtr  45302  ushrisomgr  45304  opeliun2xp  45679  map0cor  46193  thinccic  46353  bnd2d  46398