Theorem exbidv 1956

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  nfbidv  1957  2exbidv  1959  3exbidv  1960  eleq1w  2847  eleq2w  2848  eleq1d  2849  eleq2dALT  2851  clelab  2908  rexbidv2  3186  rmoeq1  3400  ceqsex2  3504  ceqsex2v  3505  alexeqg  3608  sbc2or  3751  sbc5ALT  3771  sbcex2  3802  sbcabel  3829  elpreqprlem  4826  elpreqpr  4827  eluni  4875  csbuni  4903  intab  4943  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  cbvopab1v  5189  axrep1  5239  axreplem  5240  zfrepclf  5250  axsepg  5256  sepg  5257  zfausclOLD  5259  sels  5415  euotd  5493  opeliunxp  5725  opeliun2xp  5726  brcog  5855  elrn2g  5884  dfdmf  5890  eldmg  5892  dmun  5904  dmopabelb  5910  dmopab2rex  5911  dm0rn0  5918  dfrnf  5944  elrnmpt1  5954  dfrn7  6084  brcodir  6131  dfco2a  6266  cores  6269  sbcfungOLD  6592  brprcneu  6906  brprcneuALT  6907  ssimaexg  7002  dmfco  7012  fndmdif  7072  fmptco  7162  fliftf  7354  oprabbidv  7517  cbvoprab1  7538  cbvoprab2  7539  cbvoprab12v  7541  imaeqexov  7691  uniuni  7808  dmtpos  8293  frecseq123  8338  csbfrecsg  8340  frrlem1  8342  frrlem13  8354  rdglim2  8478  ecdmn0  8808  mapsnd  8952  breng  9020  brdom2g  9022  domeng  9027  mapsnend  9102  isinf  9294  ac6sfi  9313  ordiso  9547  brwdom  9598  brwdom2  9604  zfregcl  9625  zfregclOLD  9626  inf0  9659  zfinf  9677  ttrcleq  9747  brttrcl  9751  brttrcl2  9752  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  bnd2  9993  bnd2d  10005  isinffi  10112  acneq  10161  acni  10163  aceq0  10236  aceq3lem  10238  dfac3  10239  dfac5lem4  10244  dfac8  10253  dfac9  10254  kmlem1  10268  kmlem2  10269  kmlem8  10275  kmlem10  10277  kmlem13  10280  cfval  10363  cardcf  10368  cfeq0  10373  cfsuc  10374  cff1  10375  cflim3  10379  cofsmo  10386  isfin4  10414  axcc2lem  10553  axcc4dom  10558  domtriomlem  10559  dcomex  10564  axdc2lem  10565  axdc4lem  10572  zfac  10577  ac7g  10591  ac4c  10593  ac5  10594  ac6sg  10605  weth  10612  axrepndlem1  10716  axunndlem1  10719  zfcndrep  10738  zfcndinf  10742  zfcndac  10743  gruina  10942  grothomex  10953  genpass  11133  1idpr  11153  ltexprlem3  11162  ltexprlem4  11163  ltexpri  11167  reclem2pr  11172  reclem3pr  11173  recexpr  11175  infm3  12316  nnunb  12642  axdc4uz  14167  ishashinf  14649  relexpindlem  15259  sumeq1  15900  sumeq2w  15903  sumeq2ii  15904  sumeq2sdv  15914  summo  15927  fsum  15930  fsum2dlem  15980  ntrivcvgn0  16111  ntrivcvgmullem  16114  prodeq1f  16119  prodeq1  16120  prodeq2w  16123  prodeq2ii  16124  prodeq2sdv  16135  prodmo  16147  zprod  16148  fprod  16152  fprodntriv  16153  fprod2dlem  16191  vdwapun  17196  vdwmc  17200  vdwmc2  17201  isacs  17875  dfiso2  17997  brssc  18039  isssc  18045  equivestrcsetc  18376  dirge  18827  gsumvalx  18915  gsumpropd  18917  gsumpropd2lem  18918  gsumress  18921  degenmgm2nfun  19189  gsumval3eu  20169  gsumval3lem2  20171  dprd2d2  20311  znleval  21915  neitr  23553  cmpcovf  23764  hausmapdom  23874  ptval  23944  elpt  23946  ptpjopn  23986  ptclsg  23989  ptcnp  23996  uffix2  24298  cnextf  24440  prdsxmslem2  24903  metustfbas  24931  metcld2  25683  dchrmusumlema  27877  dchrisum0lema  27898  elold  28302  lrrecfr  28386  istrkgld  28978  uvtx01vtx  30035  1loopgrvd2  30141  wspthsn  30494  iswspthn  30495  wspthsnon  30498  iswspthsnon  30502  wspthnon  30504  wlkiswwlks2  30521  wlkiswwlksupgr2  30523  wlklnwwlkln2lem  30528  wlksnwwlknvbij  30554  wspthsnwspthsnon  30562  elwwlks2on  30607  elwwlks2  30615  elwspths2spth  30616  clwlkclwwlk  30650  clwwlkvbij  30761  isgrpo  31156  adjeu  32548  iunrnmptss  33257  fcoinvbr  33297  2ndresdju  33341  fmptcof2  33349  acunirnmpt  33351  aciunf1  33355  fnpreimac  33362  fpwrelmapffslem  33420  gsumwrd2dccatlem  33737  1arithidomlem1  34171  1arithidom  34173  fmcncfil  34674  bnj865  35664  bnj1388  35774  bnj1489  35797  acwer1prclem  35892  fineqvrep  35923  fineqvac  35925  tz9.1regs  35943  onprcf1acwevdlem1  36086  satfrnmapom  36343  satf0op  36350  dmopab3rexdif  36378  prv1n  36404  rexxfr3dALT  36612  mirimanoffr  36668  eldm3  36741  opelco3  36754  elsingles  36895  funpartlem  36921  dfrdg4  36930  linedegen  37123  prodeq12sdv  37222  cbvoprab2vw  37242  cbvoprab13vw  37245  cbvmodavw  37254  cbvopab1davw  37268  cbvopab2davw  37269  cbvoprab2davw  37276  cbvoprab12davw  37279  cbvoprab23davw  37280  cbvoprab13davw  37281  cbvsumdavw  37283  cbvproddavw  37284  cbvsumdavw2  37299  cbvproddavw2  37300  finminlem  37321  filnetlem4  37384  axtco1  37476  axtco1from2  37478  axtco1g  37479  dfttc4lem1  37531  dfttc4  37533  elttcirr  37534  ttcexg  37535  regsfromregtco  37541  mh-regprimbi  37548  mh-infprim1bi  37549  mobidvALT  37984  bj-issetwt  38002  bj-inex1gALT  38052  bj-axreprepsep  38261  bj-restuni  38288  bj-finsumval0  38474  csboprabg  38521  topdifinffinlem  38538  cbveud  38563  wl-sb8eut  38778  wl-sb8eutv  38779  sdclem1  38943  fdc  38945  ismgmOLD  39050  isriscg  39184  elrnres  39476  eldm4  39479  exan3  39498  exanres  39499  eldmcnv  39543  brxrn  39581  exeupre  39689  cosseq  39714  brcoss  39719  brcoss3  39721  eldm1cossres  39748  brcosscnv  39760  islshpat  40340  lshpsmreu  40432  isopos  40503  islpln5  40858  islvol5  40902  pmapjat1  41176  dibelval3  42470  diblsmopel  42494  mapdpglem3  42998  hdmapglem7a  43250  19.9dev  43536  fimgmcyc  43864  dfac11  44330  nnoeomeqom  44575  clcnvlem  44884  dfhe3  45036  ntrneineine0lem  45344  iotasbc  45663  iotasbc2  45664  brpermmodel  46257  permaxinf2lem  46266  permac8prim  46268  nregmodel  46271  fnchoice  46320  axccdom  46508  axccd  46514  stoweidlem35  47318  stoweidlem39  47322  dfatdmfcoafv2  48597  dfatco  48599  ichexmpl1  48824  ichnreuop  48827  ichreuopeq  48828  elsprel  48830  isgrim  49253  dfgric2  49286  gricushgr  49288  gricuspgr  49289  ushggricedg  49298  isubgrgrim  49300  uhgrimisgrgric  49302  grtri  49311  grtriprop  49312  isgrtri  49314  uspgrlim  49363  grlimedgclnbgr  49366  grlimgrtri  49374  dfgrlic2  49379  dfgrlic3  49381  grilcbri2  49382  map0cor  50297  nelsubc3lem  50515  thinccic  50937  istermc  50940  termcpropd  50969  discsntermlem  51039  basrestermcfolem  51040  discsnterm  51043  cnelsubcw  51072  fuconuniqex  51117  fuconuniqex2  51118