Theorem albidv 1917

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1863 and albid 2219. (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 1907	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1863	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  nfbidv  1919  2albidv  1920  sbjust  2060  sbequ  2080  sb6  2082  ax12wdemo  2132  sb4b  2477  mojust  2536  mof  2560  eujust  2568  eujustALT  2569  eu6lem  2570  euf  2573  axextg  2707  axextmo  2709  eqeq1dALT  2737  nfceqdf  2898  drnfc1  2922  drnfc2  2923  ralbidv2  3171  ralxpxfr2d  3645  alexeqg  3650  pm13.183  3665  elab6g  3668  elabd2  3669  eqeu  3714  mo2icl  3722  euind  3732  reuind  3761  cdeqal  3777  sbcal  3854  sbccomlem  3877  sbcabel  3886  csbiebg  3940  ssconb  4151  reldisj  4458  sbcssg  4525  elint  4956  axrep1  5285  axreplem  5286  axrep2  5287  axrep4OLD  5291  zfrepclf  5296  axsepg  5302  zfauscl  5303  bm1.3iiOLD  5307  al0ssb  5313  eusv1  5396  euotd  5522  freq1  5655  frsn  5775  iota5  6545  dffun2  6572  sbcfung  6591  funimass4  6972  dffo3  7121  dffo3f  7125  eufnfv  7248  dff13  7274  fnssintima  7381  nfriotadw  7395  imaeqalov  7671  tfisi  7879  dfom2  7888  elom  7889  xpord3inddlem  8177  seqomlem2  8489  findcard  9201  findcard2  9202  pssnn  9206  ssfi  9211  findcard3  9315  findcard3OLD  9316  fiint  9363  fiintOLD  9364  inf0  9658  axinf2  9677  ttrclss  9757  ttrclselem2  9763  tz9.1  9766  karden  9932  aceq0  10155  dfac5  10166  zfac  10497  brdom3  10565  axpowndlem3  10636  zfcndrep  10651  zfcndac  10656  elgch  10659  engch  10665  axgroth3  10868  axgroth4  10869  elnp  11024  elnpi  11025  infm3  12224  fz1sbc  13636  uzrdgfni  13995  trclfvcotr  15044  relexpindlem  15098  vdwmc2  17012  ramtlecl  17033  ramval  17041  ramub  17046  rami  17048  ramcl  17062  mreexexd  17692  mplsubglem  22036  mpllsslem  22037  ismhp3  22163  istopg  22916  1stccn  23486  iskgen3  23572  fbfinnfr  23864  cnextfun  24087  metcld  25353  metcld2  25354  noseqrdgfn  28326  chlimi  31262  nmcexi  32054  disjxun0  32593  disjrdx  32610  funcnvmpt  32683  mclsssvlem  35546  mclsval  35547  mclsind  35554  elintfv  35745  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  dfon2  35773  sscoid  35894  sbequbidv  36196  disjeq12dv  36197  ixpeq12dv  36198  cbvsbdavw  36236  cbvsbdavw2  36237  cbvdisjdavw  36250  cbvdisjdavw2  36271  trer  36298  bj-ssblem1  36636  bj-ax12  36639  mobidvALT  36839  bj-sbceqgALT  36884  bj-nuliota  37039  bj-bm1.3ii  37046  wl-ax12v2cl  37486  wl-mo2t  37555  isass  37832  releccnveq  38239  ecin0  38333  inecmo  38336  alrmomodm  38340  extssr  38490  eltrrels3  38561  eleqvrels3  38574  axc11n-16  38919  cdlemefrs29bpre0  40378  eu6w  42662  unielss  43206  orddif0suc  43257  elmapintab  43585  cnvcnvintabd  43589  iunrelexpuztr  43708  ntrneiiso  44080  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  mnuop123d  44257  pm14.122b  44418  iotavalb  44425  trsbc  44537  eusnsn  46975  aiota0def  47045  ichbidv  47377  mof0  48667  eufsnlem  48670  setrecseq  48915  setrec1lem1  48917  setrec2fun  48922  setrec2lem2  48924