Theorem exbidv 1929

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

Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-ex 1788

This theorem is referenced by:  nfbidv  1930  2exbidv  1932  3exbidv  1933  eleq1w  2813  eleq2w  2814  eleq1d  2815  eleq2dALT  2817  clelab  2873  nfcriOLD  2887  rexbidv2  3204  cgsex4g  3442  ceqsex2  3448  ceqsex2v  3449  alexeqg  3548  sbc2or  3692  sbc5ALT  3712  sbcex2  3748  sbcabel  3777  elpreqprlem  4762  elpreqpr  4763  eluni  4808  csbuni  4836  intab  4875  cbvopab1  5113  cbvopab1g  5114  cbvopab1s  5116  axrep1  5165  axreplem  5166  zfrepclf  5172  axsepg  5178  zfauscl  5179  euotd  5381  opeliunxp  5601  brcog  5720  elrn2g  5744  dfdmf  5750  eldmg  5752  dmopabelb  5770  dmopab2rex  5771  dfrnf  5804  elrnmpt1  5812  brcodir  5964  dfco2a  6090  cores  6093  sbcfung  6382  brprcneu  6686  fvprc  6687  ssimaexg  6775  dmfco  6785  fndmdif  6840  fmptco  6922  fliftf  7102  cbvoprab1  7276  cbvoprab2  7277  uniuni  7525  dmtpos  7958  frecseq123  8002  frrlem1  8005  frrlem13  8017  wrecseq123  8026  wfrlem1  8032  wfrlem3a  8035  wfrlem15  8047  rdglim2  8146  ecdmn0  8416  mapsnd  8545  breng  8613  brenOLD  8615  brdomg  8616  domeng  8620  mapsnend  8691  isinf  8867  ac6sfi  8893  ordiso  9110  brwdom  9161  brwdom2  9167  zfregcl  9188  inf0  9214  zfinf  9232  bnd2  9474  isinffi  9573  acneq  9622  acni  9624  aceq0  9697  aceq3lem  9699  dfac3  9700  dfac5lem4  9705  dfac8  9714  dfac9  9715  kmlem1  9729  kmlem2  9730  kmlem8  9736  kmlem10  9738  kmlem13  9741  cfval  9826  cardcf  9831  cfeq0  9835  cfsuc  9836  cff1  9837  cflim3  9841  cofsmo  9848  isfin4  9876  axcc2lem  10015  axcc4dom  10020  domtriomlem  10021  dcomex  10026  axdc2lem  10027  axdc4lem  10034  zfac  10039  ac7g  10053  ac4c  10055  ac5  10056  ac6sg  10067  weth  10074  axrepndlem1  10171  axunndlem1  10174  zfcndrep  10193  zfcndinf  10197  zfcndac  10198  gruina  10397  grothomex  10408  genpass  10588  1idpr  10608  ltexprlem3  10617  ltexprlem4  10618  ltexpri  10622  reclem2pr  10627  reclem3pr  10628  recexpr  10630  infm3  11756  nnunb  12051  axdc4uz  13522  ishashinf  13994  relexpindlem  14591  sumeq1  15217  sumeq2w  15221  sumeq2ii  15222  summo  15246  fsum  15249  fsum2dlem  15297  ntrivcvgn0  15425  ntrivcvgmullem  15428  prodeq1f  15433  prodeq2w  15437  prodeq2ii  15438  prodmo  15461  zprod  15462  fprod  15466  fprodntriv  15467  fprod2dlem  15505  vdwapun  16490  vdwmc  16494  vdwmc2  16495  isacs  17108  dfiso2  17231  brssc  17273  isssc  17279  equivestrcsetc  17613  dirge  18063  gsumvalx  18102  gsumpropd  18104  gsumpropd2lem  18105  gsumress  18108  gsumval3eu  19243  gsumval3lem2  19245  dprd2d2  19385  znleval  20473  neitr  22031  cmpcovf  22242  hausmapdom  22351  ptval  22421  elpt  22423  ptpjopn  22463  ptclsg  22466  ptcnp  22473  uffix2  22775  cnextf  22917  prdsxmslem2  23381  metustfbas  23409  metcld2  24158  dchrmusumlema  26328  dchrisum0lema  26349  istrkgld  26504  uvtx01vtx  27439  1loopgrvd2  27545  wspthsn  27886  iswspthn  27887  wspthsnon  27890  iswspthsnon  27894  wspthnon  27896  wlkiswwlks2  27913  wlkiswwlksupgr2  27915  wlklnwwlkln2lem  27920  wlksnwwlknvbij  27946  wspthsnwspthsnon  27954  elwwlks2on  27997  elwwlks2  28004  elwspths2spth  28005  clwlkclwwlk  28039  clwwlkvbij  28150  isgrpo  28532  adjeu  29924  iunrnmptss  30578  fcoinvbr  30620  2ndresdju  30659  fmptcof2  30668  acunirnmpt  30670  acunirnmpt2  30671  acunirnmpt2f  30672  aciunf1  30674  fnpreimac  30682  fpwrelmapffslem  30741  fmcncfil  31549  bnj865  32570  bnj1388  32680  bnj1489  32703  fineqvrep  32731  fineqvac  32733  satfrnmapom  32999  satf0op  33006  dmopab3rexdif  33034  prv1n  33060  imaeqsexv  33360  eldm3  33398  opelco3  33419  elold  33739  lrrecfr  33786  elsingles  33906  funpartlem  33930  dfrdg4  33939  linedegen  34131  finminlem  34193  filnetlem4  34256  mobidvALT  34727  bj-issetwt  34745  bj-restuni  34952  bj-finsumval0  35140  csbwrecsg  35184  csboprabg  35187  topdifinffinlem  35204  cbveud  35229  wl-sb8eut  35418  sdclem1  35587  fdc  35589  ismgmOLD  35694  isriscg  35828  eldm4  36095  exan3  36115  exanres  36116  eldmcnv  36166  brxrn  36190  cosseq  36235  brcoss  36240  brcoss3  36242  eldm1cossres  36264  brcosscnv  36276  islshpat  36717  lshpsmreu  36809  isopos  36880  islpln5  37235  islvol5  37279  pmapjat1  37553  dibelval3  38847  diblsmopel  38871  mapdpglem3  39375  hdmapglem7a  39627  19.9dev  39842  dfac11  40531  clcnvlem  40848  dfhe3  41001  ntrneineine0lem  41311  iotasbc  41651  iotasbc2  41652  fnchoice  42186  axccdom  42376  axccd  42382  stoweidlem35  43194  stoweidlem39  43198  dfatdmfcoafv2  44361  dfatco  44363  ichexmpl1  44537  ichnreuop  44540  ichreuopeq  44541  elsprel  44543  isomgr  44891  isomgreqve  44893  isomushgr  44894  isomuspgr  44902  isomgrsym  44904  isomgrtr  44907  ushrisomgr  44909  opeliun2xp  45284  map0cor  45798  thinccic  45958  bnd2d  46001