Theorem albidv 1919

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1865 and albid 2223. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
albidv	⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem albidv

Step	Hyp	Ref	Expression
1		ax-5 1909	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1865	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  nfbidv  1921  2albidv  1922  sbjust  2063  sbequ  2083  sb6  2085  ax12wdemo  2135  sb4b  2483  mojust  2542  mof  2566  eujust  2574  eujustALT  2575  eu6lem  2576  euf  2579  axextg  2713  axextmo  2715  eqeq1dALT  2743  nfceqdf  2904  drnfc1  2928  drnfc1OLD  2929  drnfc2  2930  drnfc2OLD  2931  ralbidv2  3180  ralxpxfr2d  3659  alexeqg  3664  pm13.183  3679  elab6g  3682  elabd2  3683  eqeu  3728  mo2icl  3736  euind  3746  reuind  3775  cdeqal  3791  sbcal  3868  sbccomlem  3891  sbcabel  3900  csbiebg  3954  ssconb  4165  reldisj  4476  sbcssg  4543  elint  4976  axrep1  5304  axreplem  5305  axrep2  5306  axrep4  5308  zfrepclf  5312  axsepg  5318  zfauscl  5319  bm1.3ii  5320  al0ssb  5326  eusv1  5409  euotd  5532  freq1  5667  frsn  5787  iota5  6556  dffun2  6583  sbcfung  6602  funimass4  6986  dffo3  7136  dffo3f  7140  eufnfv  7266  dff13  7292  fnssintima  7398  nfriotadw  7412  imaeqalov  7689  tfisi  7896  dfom2  7905  elom  7906  xpord3inddlem  8195  seqomlem2  8507  findcard  9229  findcard2  9230  pssnn  9234  ssfi  9240  findcard3  9346  findcard3OLD  9347  fiint  9394  fiintOLD  9395  inf0  9690  axinf2  9709  ttrclss  9789  ttrclselem2  9795  tz9.1  9798  karden  9964  aceq0  10187  dfac5  10198  zfac  10529  brdom3  10597  axpowndlem3  10668  zfcndrep  10683  zfcndac  10688  elgch  10691  engch  10697  axgroth3  10900  axgroth4  10901  elnp  11056  elnpi  11057  infm3  12254  fz1sbc  13660  uzrdgfni  14009  trclfvcotr  15058  relexpindlem  15112  vdwmc2  17026  ramtlecl  17047  ramval  17055  ramub  17060  rami  17062  ramcl  17076  mreexexd  17706  mplsubglem  22042  mpllsslem  22043  ismhp3  22169  istopg  22922  1stccn  23492  iskgen3  23578  fbfinnfr  23870  cnextfun  24093  metcld  25359  metcld2  25360  noseqrdgfn  28330  chlimi  31266  nmcexi  32058  disjxun0  32596  disjrdx  32613  funcnvmpt  32685  mclsssvlem  35530  mclsval  35531  mclsind  35538  elintfv  35728  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  sscoid  35877  sbequbidv  36180  disjeq12dv  36181  ixpeq12dv  36182  cbvsbdavw  36220  cbvsbdavw2  36221  cbvdisjdavw  36234  cbvdisjdavw2  36255  trer  36282  bj-ssblem1  36620  bj-ax12  36623  mobidvALT  36823  bj-sbceqgALT  36868  bj-nuliota  37023  bj-bm1.3ii  37030  wl-mo2t  37529  isass  37806  releccnveq  38214  ecin0  38308  inecmo  38311  alrmomodm  38315  extssr  38465  eltrrels3  38536  eleqvrels3  38549  axc11n-16  38894  cdlemefrs29bpre0  40353  eu6w  42631  unielss  43179  orddif0suc  43230  elmapintab  43558  cnvcnvintabd  43562  iunrelexpuztr  43681  ntrneiiso  44053  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  mnuop123d  44231  pm14.122b  44392  iotavalb  44399  trsbc  44511  eusnsn  46941  aiota0def  47011  ichbidv  47327  mof0  48551  eufsnlem  48554  setrecseq  48777  setrec1lem1  48779  setrec2fun  48784  setrec2lem2  48786