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  2817  eleq2w  2818  eleq1d  2819  eleq2dALT  2821  clelab  2880  nfcriOLD  2894  rexbidv2  3175  rmoeq1  3415  cgsex4gOLD  3522  ceqsex2  3530  ceqsex2v  3531  alexeqg  3639  sbc2or  3786  sbc5ALT  3806  sbcex2  3842  sbcabel  3872  elpreqprlem  4866  elpreqpr  4867  eluni  4911  csbuni  4940  intab  4982  cbvopab1  5223  cbvopab1g  5224  cbvopab1s  5226  cbvopab1v  5227  axrep1  5286  axreplem  5287  zfrepclf  5294  axsepg  5300  zfauscl  5301  sels  5438  euotd  5513  opeliunxp  5742  brcog  5865  elrn2g  5889  dfdmf  5895  eldmg  5897  dmopabelb  5915  dmopab2rex  5916  dfrnf  5948  elrnmpt1  5956  brcodir  6118  dfco2a  6243  cores  6246  sbcfung  6570  brprcneu  6879  brprcneuALT  6880  ssimaexg  6975  dmfco  6985  fndmdif  7041  fmptco  7124  fliftf  7309  imaeqsexv  7357  oprabbidv  7472  cbvoprab1  7493  cbvoprab2  7494  imaeqexov  7642  uniuni  7746  dmtpos  8220  frecseq123  8264  csbfrecsg  8266  frrlem1  8268  frrlem13  8280  wrecseq123OLD  8297  wfrlem1OLD  8305  wfrlem3OLDa  8308  wfrlem15OLD  8320  rdglim2  8429  ecdmn0  8747  mapsnd  8877  breng  8945  brenOLD  8947  brdom2g  8948  brdomgOLD  8950  domeng  8955  mapsnend  9033  isinf  9257  isinfOLD  9258  ac6sfi  9284  ordiso  9508  brwdom  9559  brwdom2  9565  zfregcl  9586  inf0  9613  zfinf  9631  ttrcleq  9701  brttrcl  9705  brttrcl2  9706  ssttrcl  9707  ttrcltr  9708  ttrclss  9712  ttrclselem2  9718  bnd2  9885  isinffi  9984  acneq  10035  acni  10037  aceq0  10110  aceq3lem  10112  dfac3  10113  dfac5lem4  10118  dfac8  10127  dfac9  10128  kmlem1  10142  kmlem2  10143  kmlem8  10149  kmlem10  10151  kmlem13  10154  cfval  10239  cardcf  10244  cfeq0  10248  cfsuc  10249  cff1  10250  cflim3  10254  cofsmo  10261  isfin4  10289  axcc2lem  10428  axcc4dom  10433  domtriomlem  10434  dcomex  10439  axdc2lem  10440  axdc4lem  10447  zfac  10452  ac7g  10466  ac4c  10468  ac5  10469  ac6sg  10480  weth  10487  axrepndlem1  10584  axunndlem1  10587  zfcndrep  10606  zfcndinf  10610  zfcndac  10611  gruina  10810  grothomex  10821  genpass  11001  1idpr  11021  ltexprlem3  11030  ltexprlem4  11031  ltexpri  11035  reclem2pr  11040  reclem3pr  11041  recexpr  11043  infm3  12170  nnunb  12465  axdc4uz  13946  ishashinf  14421  relexpindlem  15007  sumeq1  15632  sumeq2w  15635  sumeq2ii  15636  summo  15660  fsum  15663  fsum2dlem  15713  ntrivcvgn0  15841  ntrivcvgmullem  15844  prodeq1f  15849  prodeq2w  15853  prodeq2ii  15854  prodmo  15877  zprod  15878  fprod  15882  fprodntriv  15883  fprod2dlem  15921  vdwapun  16904  vdwmc  16908  vdwmc2  16909  isacs  17592  dfiso2  17716  brssc  17758  isssc  17764  equivestrcsetc  18101  dirge  18553  gsumvalx  18592  gsumpropd  18594  gsumpropd2lem  18595  gsumress  18598  gsumval3eu  19767  gsumval3lem2  19769  dprd2d2  19909  znleval  21102  neitr  22676  cmpcovf  22887  hausmapdom  22996  ptval  23066  elpt  23068  ptpjopn  23108  ptclsg  23111  ptcnp  23118  uffix2  23420  cnextf  23562  prdsxmslem2  24030  metustfbas  24058  metcld2  24816  dchrmusumlema  26986  dchrisum0lema  27007  elold  27354  lrrecfr  27417  istrkgld  27700  uvtx01vtx  28644  1loopgrvd2  28750  wspthsn  29092  iswspthn  29093  wspthsnon  29096  iswspthsnon  29100  wspthnon  29102  wlkiswwlks2  29119  wlkiswwlksupgr2  29121  wlklnwwlkln2lem  29126  wlksnwwlknvbij  29152  wspthsnwspthsnon  29160  elwwlks2on  29203  elwwlks2  29210  elwspths2spth  29211  clwlkclwwlk  29245  clwwlkvbij  29356  isgrpo  29738  adjeu  31130  iunrnmptss  31785  fcoinvbr  31824  2ndresdju  31862  fmptcof2  31870  acunirnmpt  31872  acunirnmpt2  31873  acunirnmpt2f  31874  aciunf1  31876  fnpreimac  31884  fpwrelmapffslem  31945  fmcncfil  32900  bnj865  33923  bnj1388  34033  bnj1489  34056  fineqvrep  34084  fineqvac  34086  satfrnmapom  34350  satf0op  34357  dmopab3rexdif  34385  prv1n  34411  eldm3  34720  opelco3  34735  elsingles  34879  funpartlem  34903  dfrdg4  34912  linedegen  35104  finminlem  35192  filnetlem4  35255  mobidvALT  35725  bj-issetwt  35743  bj-restuni  35967  bj-finsumval0  36155  csboprabg  36200  topdifinffinlem  36217  cbveud  36242  wl-sb8eut  36431  sdclem1  36600  fdc  36602  ismgmOLD  36707  isriscg  36841  elrnres  37128  eldm4  37131  exan3  37152  exanres  37153  eldmcnv  37203  brxrn  37233  cosseq  37285  brcoss  37290  brcoss3  37292  eldm1cossres  37319  brcosscnv  37331  islshpat  37876  lshpsmreu  37968  isopos  38039  islpln5  38395  islvol5  38439  pmapjat1  38713  dibelval3  40007  diblsmopel  40031  mapdpglem3  40535  hdmapglem7a  40787  19.9dev  41025  dfac11  41790  nnoeomeqom  42048  clcnvlem  42360  dfhe3  42512  ntrneineine0lem  42820  iotasbc  43164  iotasbc2  43165  fnchoice  43699  axccdom  43907  axccd  43914  stoweidlem35  44738  stoweidlem39  44742  dfatdmfcoafv2  45949  dfatco  45951  ichexmpl1  46124  ichnreuop  46127  ichreuopeq  46128  elsprel  46130  isomgr  46478  isomgreqve  46480  isomushgr  46481  isomuspgr  46489  isomgrsym  46491  isomgrtr  46494  ushrisomgr  46496  opeliun2xp  46962  map0cor  47475  thinccic  47635  bnd2d  47680