Theorem albidv 1953

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1899 and albid 2259. (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  2505  mojust  2564  mof  2589  eujust  2597  eujustALT  2598  eu6lem  2599  euf  2602  axextg  2735  axextmo  2737  eqeq1dALT  2764  nfceqdf  2919  drnfc1  2942  drnfc2  2943  ralbidv2  3182  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  zfrepclf  5244  axsepg  5250  sepg  5251  zfausclOLD  5253  al0ssb  5262  eusv1  5353  euotd  5486  freq1  5618  frsn  5739  iota5  6521  dffun2  6548  sbcfungOLD  6564  funimass4  6949  funcnvmpt  6995  dffo3  7102  dffo3f  7106  eufnfv  7235  dff13  7258  fnssintima  7372  nfriotadw  7385  imaeqalov  7660  tfisi  7870  dfom2  7879  elom  7880  xpord3inddlem  8171  seqomlem2  8461  findcard  9179  findcard2  9180  pssnn  9184  ssfi  9188  findcard3  9274  fiint  9318  elirrv  9591  inf0  9622  axinf2  9641  ttrclss  9721  ttrclselem2  9727  tz9.1  9730  kardenOLD  9960  setrec1lem1  9966  setrec2fun  9973  setrec2lem2  9976  aceq0  10197  dfac5  10207  zfac  10538  brdom3  10607  axpowndlem3  10684  zfcndrep  10699  zfcndac  10704  elgch  10707  engch  10713  axgroth3  10916  axgroth4  10917  elnp  11072  elnpi  11073  infm3  12276  fz1sbc  13734  uzrdgfni  14101  trclfvcotr  15162  relexpindlem  15216  vdwmc2  17157  ramtlecl  17178  ramval  17186  ramub  17191  rami  17193  ramcl  17207  mreexexd  17822  mplsubglem  22306  mpllsslem  22307  ismhp3  22463  istopg  23213  1stccn  23782  iskgen3  23868  fbfinnfr  24160  cnextfun  24383  metcld  25627  metcld2  25628  noseqrdgfn  28692  chlimi  31836  nmcexi  32628  disjxun0  33168  disjrdx  33185  axprALT2  35734  tz9.1regs  35802  axsepg5  35812  elkarden  35823  mclsssvlem  36327  mclsval  36328  mclsind  36335  elintfv  36530  dfon2lem6  36550  dfon2lem7  36551  dfon2lem8  36552  dfon2  36554  sscoid  36675  sbequbidv  37003  disjeq12dv  37004  ixpeq12dv  37005  cbvsbdavw  37043  cbvsbdavw2  37044  cbvdisjdavw  37057  cbvdisjdavw2  37078  trer  37104  axtcond  37266  axuntco  37267  regsfromregtco  37326  mh-regprimbi  37333  bj-ssblem1  37553  bj-ax12  37556  mobidvALT  37769  bj-sbceqgALT  37814  bj-inex1gALT  37837  bj-nuliota  37972  bj-bm1.3ii  37979  wl-ax12v2cl  38429  wl-mo2t  38507  findcard4  38632  isass  38780  releccnveq  39193  ecin0  39284  inecmo  39287  alrmomodm  39291  raldmqseu  39297  extssr  39521  eltrrels3  39596  eleqvrels3  39609  axc11n-16  39995  cdlemefrs29bpre0  41453  eu6w  43687  unielss  44219  orddif0suc  44269  elmapintab  44595  cnvcnvintabd  44599  iunrelexpuztr  44718  ntrneiiso  45090  ntrneik2  45091  ntrneix2  45092  ntrneikb  45093  mnuop123d  45245  pm14.122b  45406  iotavalb  45413  trsbc  45522  permaxnul  45997  permaxpow  45998  permaxpr  45999  permaxun  46000  permaxinf2lem  46001  permac8prim  46003  nregmodel  46006  eusnsn  48095  aiota0def  48165  ichbidv  48534  mof0  49947  eufsnlem  49950  termcarweu  50635  setrecseq  50787