Theorem albidv 1953

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568

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 1943

This proof depends on definitions:  df-bi 210

This theorem is used by:  nfbidv  1955  2albidv  1956  sbjust  2098  sbequ  2120  sb6  2122  ax12wdemo  2172  sb4b  2504  mojust  2563  mof  2588  eujust  2596  eujustALT  2597  eu6lem  2598  euf  2601  axextg  2734  axextmo  2736  eqeq1dALT  2763  nfceqdf  2918  drnfc1  2941  drnfc2  2942  ralbidv2  3181  ralxpxfr2d  3600  alexeqg  3605  pm13.183  3620  elab6g  3623  elabd2  3624  eqeu  3664  mo2icl  3672  euind  3682  reuind  3711  cdeqal  3727  sbcal  3798  sbccomlem  3817  sbcabel  3825  csbiebg  3879  ssconb  4089  reldisj  4406  sbcssg  4477  elint  4913  axrep1  5233  axreplem  5234  axrep2  5235  axrep4OLD  5239  zfrepclf  5246  axsepg  5252  sepg  5253  zfausclOLD  5255  bm1.3iiOLD  5259  al0ssb  5265  eusv1  5356  euotd  5490  freq1  5622  frsn  5743  iota5  6516  dffun2  6543  sbcfungOLD  6558  funimass4  6943  funcnvmpt  6989  dffo3  7096  dffo3f  7100  eufnfv  7229  dff13  7252  fnssintima  7366  nfriotadw  7379  imaeqalov  7654  tfisi  7856  dfom2  7865  elom  7866  xpord3inddlem  8153  seqomlem2  8443  findcard  9161  findcard2  9162  pssnn  9166  ssfi  9170  findcard3  9256  fiint  9299  elirrv  9572  inf0  9603  axinf2  9622  ttrclss  9702  ttrclselem2  9708  tz9.1  9711  kardenOLD  9902  aceq0  10124  dfac5  10134  zfac  10465  brdom3  10534  axpowndlem3  10611  zfcndrep  10626  zfcndac  10631  elgch  10634  engch  10640  axgroth3  10843  axgroth4  10844  elnp  10999  elnpi  11000  infm3  12201  fz1sbc  13658  uzrdgfni  14025  trclfvcotr  15085  relexpindlem  15139  vdwmc2  17074  ramtlecl  17095  ramval  17103  ramub  17108  rami  17110  ramcl  17124  mreexexd  17739  mplsubglem  22216  mpllsslem  22217  ismhp3  22373  istopg  23123  1stccn  23692  iskgen3  23778  fbfinnfr  24070  cnextfun  24293  metcld  25537  metcld2  25538  noseqrdgfn  28574  chlimi  31718  nmcexi  32510  disjxun0  33050  disjrdx  33067  axprALT2  35620  tz9.1regs  35663  axsepg5  35673  elkarden  35684  mclsssvlem  36144  mclsval  36145  mclsind  36152  elintfv  36347  dfon2lem6  36368  dfon2lem7  36369  dfon2lem8  36370  dfon2  36372  sscoid  36493  sbequbidv  36837  disjeq12dv  36838  ixpeq12dv  36839  cbvsbdavw  36877  cbvsbdavw2  36878  cbvdisjdavw  36891  cbvdisjdavw2  36912  trer  36938  axtcond  37100  axuntco  37101  regsfromregtco  37160  mh-regprimbi  37167  bj-ssblem1  37387  bj-ax12  37390  mobidvALT  37603  bj-sbceqgALT  37648  bj-inex1gALT  37671  bj-nuliota  37804  bj-bm1.3ii  37811  wl-ax12v2cl  38263  wl-mo2t  38341  findcard4  38466  isass  38599  releccnveq  39012  ecin0  39103  inecmo  39106  alrmomodm  39110  raldmqseu  39116  extssr  39340  eltrrels3  39415  eleqvrels3  39428  axc11n-16  39814  cdlemefrs29bpre0  41272  eu6w  43525  unielss  44062  orddif0suc  44112  elmapintab  44439  cnvcnvintabd  44443  iunrelexpuztr  44562  ntrneiiso  44934  ntrneik2  44935  ntrneix2  44936  ntrneikb  44937  mnuop123d  45089  pm14.122b  45250  iotavalb  45257  trsbc  45366  permaxnul  45834  permaxpow  45835  permaxpr  45836  permaxun  45837  permaxinf2lem  45838  permac8prim  45840  nregmodel  45843  eusnsn  47917  aiota0def  47987  ichbidv  48356  mof0  49769  eufsnlem  49772  termcarweu  50457  setrecseq  50614  setrec1lem1  50616  setrec2fun  50621  setrec2lem2  50623