Theorem exbidv 1925

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1871 and exbid 2219. (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 1783

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

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

This theorem is referenced by:  nfbidv  1926  2exbidv  1928  3exbidv  1929  eleq1w  2821  eleq2w  2822  eleq1d  2823  eleq2dALT  2825  clelab  2882  nfcriOLD  2896  rexbidv2  3223  cgsex4g  3466  ceqsex2  3472  ceqsex2v  3473  alexeqg  3573  sbc2or  3720  sbc5ALT  3740  sbcex2  3777  sbcabel  3807  elpreqprlem  4793  elpreqpr  4794  eluni  4839  csbuni  4867  intab  4906  cbvopab1  5145  cbvopab1g  5146  cbvopab1s  5148  cbvopab1v  5149  axrep1  5206  axreplem  5207  zfrepclf  5213  axsepg  5219  zfauscl  5220  euotd  5421  opeliunxp  5645  brcog  5764  elrn2g  5788  dfdmf  5794  eldmg  5796  dmopabelb  5814  dmopab2rex  5815  dfrnf  5848  elrnmpt1  5856  brcodir  6013  dfco2a  6139  cores  6142  sbcfung  6442  brprcneu  6747  fvprc  6748  ssimaexg  6836  dmfco  6846  fndmdif  6901  fmptco  6983  fliftf  7166  oprabbidv  7319  cbvoprab1  7340  cbvoprab2  7341  uniuni  7590  dmtpos  8025  frecseq123  8069  csbfrecsg  8071  frrlem1  8073  frrlem13  8085  wrecseq123OLD  8102  wfrlem1OLD  8110  wfrlem3OLDa  8113  wfrlem15OLD  8125  rdglim2  8234  ecdmn0  8503  mapsnd  8632  breng  8700  brenOLD  8702  brdomg  8703  domeng  8707  mapsnend  8780  isinf  8965  ac6sfi  8988  ordiso  9205  brwdom  9256  brwdom2  9262  zfregcl  9283  inf0  9309  zfinf  9327  bnd2  9582  isinffi  9681  acneq  9730  acni  9732  aceq0  9805  aceq3lem  9807  dfac3  9808  dfac5lem4  9813  dfac8  9822  dfac9  9823  kmlem1  9837  kmlem2  9838  kmlem8  9844  kmlem10  9846  kmlem13  9849  cfval  9934  cardcf  9939  cfeq0  9943  cfsuc  9944  cff1  9945  cflim3  9949  cofsmo  9956  isfin4  9984  axcc2lem  10123  axcc4dom  10128  domtriomlem  10129  dcomex  10134  axdc2lem  10135  axdc4lem  10142  zfac  10147  ac7g  10161  ac4c  10163  ac5  10164  ac6sg  10175  weth  10182  axrepndlem1  10279  axunndlem1  10282  zfcndrep  10301  zfcndinf  10305  zfcndac  10306  gruina  10505  grothomex  10516  genpass  10696  1idpr  10716  ltexprlem3  10725  ltexprlem4  10726  ltexpri  10730  reclem2pr  10735  reclem3pr  10736  recexpr  10738  infm3  11864  nnunb  12159  axdc4uz  13632  ishashinf  14105  relexpindlem  14702  sumeq1  15328  sumeq2w  15332  sumeq2ii  15333  summo  15357  fsum  15360  fsum2dlem  15410  ntrivcvgn0  15538  ntrivcvgmullem  15541  prodeq1f  15546  prodeq2w  15550  prodeq2ii  15551  prodmo  15574  zprod  15575  fprod  15579  fprodntriv  15580  fprod2dlem  15618  vdwapun  16603  vdwmc  16607  vdwmc2  16608  isacs  17277  dfiso2  17401  brssc  17443  isssc  17449  equivestrcsetc  17785  dirge  18236  gsumvalx  18275  gsumpropd  18277  gsumpropd2lem  18278  gsumress  18281  gsumval3eu  19420  gsumval3lem2  19422  dprd2d2  19562  znleval  20674  neitr  22239  cmpcovf  22450  hausmapdom  22559  ptval  22629  elpt  22631  ptpjopn  22671  ptclsg  22674  ptcnp  22681  uffix2  22983  cnextf  23125  prdsxmslem2  23591  metustfbas  23619  metcld2  24376  dchrmusumlema  26546  dchrisum0lema  26567  istrkgld  26724  uvtx01vtx  27667  1loopgrvd2  27773  wspthsn  28114  iswspthn  28115  wspthsnon  28118  iswspthsnon  28122  wspthnon  28124  wlkiswwlks2  28141  wlkiswwlksupgr2  28143  wlklnwwlkln2lem  28148  wlksnwwlknvbij  28174  wspthsnwspthsnon  28182  elwwlks2on  28225  elwwlks2  28232  elwspths2spth  28233  clwlkclwwlk  28267  clwwlkvbij  28378  isgrpo  28760  adjeu  30152  iunrnmptss  30806  fcoinvbr  30848  2ndresdju  30887  fmptcof2  30896  acunirnmpt  30898  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1  30902  fnpreimac  30910  fpwrelmapffslem  30969  fmcncfil  31783  bnj865  32803  bnj1388  32913  bnj1489  32936  fineqvrep  32964  fineqvac  32966  satfrnmapom  33232  satf0op  33239  dmopab3rexdif  33267  prv1n  33293  imaeqsexv  33593  eldm3  33634  opelco3  33655  ttrcleq  33695  brttrcl  33699  brttrcl2  33700  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  ttrclselem2  33712  elold  33980  lrrecfr  34027  elsingles  34147  funpartlem  34171  dfrdg4  34180  linedegen  34372  finminlem  34434  filnetlem4  34497  mobidvALT  34968  bj-issetwt  34986  bj-restuni  35195  bj-finsumval0  35383  csboprabg  35428  topdifinffinlem  35445  cbveud  35470  wl-sb8eut  35659  sdclem1  35828  fdc  35830  ismgmOLD  35935  isriscg  36069  eldm4  36336  exan3  36356  exanres  36357  eldmcnv  36407  brxrn  36431  cosseq  36476  brcoss  36481  brcoss3  36483  eldm1cossres  36505  brcosscnv  36517  islshpat  36958  lshpsmreu  37050  isopos  37121  islpln5  37476  islvol5  37520  pmapjat1  37794  dibelval3  39088  diblsmopel  39112  mapdpglem3  39616  hdmapglem7a  39868  19.9dev  40106  dfac11  40803  clcnvlem  41120  dfhe3  41272  ntrneineine0lem  41582  iotasbc  41926  iotasbc2  41927  fnchoice  42461  axccdom  42651  axccd  42657  stoweidlem35  43466  stoweidlem39  43470  dfatdmfcoafv2  44633  dfatco  44635  ichexmpl1  44809  ichnreuop  44812  ichreuopeq  44813  elsprel  44815  isomgr  45163  isomgreqve  45165  isomushgr  45166  isomuspgr  45174  isomgrsym  45176  isomgrtr  45179  ushrisomgr  45181  opeliun2xp  45556  map0cor  46070  thinccic  46230  bnd2d  46273