Theorem albidv 1953

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1899 and albid 2261. (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  2173  sb4b  2509  mojust  2568  mof  2593  eujust  2601  eujustALT  2602  eu6lem  2603  euf  2606  axextg  2739  axextmo  2741  eqeq1dALT  2768  nfceqdf  2923  drnfc1  2946  drnfc2  2947  ralbidv2  3186  ralxpxfr2d  3607  alexeqg  3612  pm13.183  3627  elab6g  3630  elabd2  3631  eqeu  3671  mo2icl  3679  euind  3689  reuind  3718  cdeqal  3734  sbcal  3805  sbccomlem  3824  sbcabel  3832  csbiebg  3886  ssconb  4096  reldisj  4413  sbcssg  4484  elint  4920  axrep1  5241  axreplem  5242  axrep2  5243  axrep4OLD  5247  zfrepclf  5254  axsepg  5260  sepg  5261  zfausclOLD  5263  bm1.3iiOLD  5267  al0ssb  5273  eusv1  5364  euotd  5498  freq1  5630  frsn  5751  iota5  6523  dffun2  6550  sbcfung  6564  funimass4  6949  funcnvmpt  6995  dffo3  7101  dffo3f  7105  eufnfv  7234  dff13  7257  fnssintima  7371  nfriotadw  7384  imaeqalov  7659  tfisi  7861  dfom2  7870  elom  7871  xpord3inddlem  8156  seqomlem2  8444  findcard  9155  findcard2  9156  pssnn  9160  ssfi  9164  findcard3  9250  fiint  9293  elirrv  9566  inf0  9597  axinf2  9616  ttrclss  9696  ttrclselem2  9702  tz9.1  9705  kardenOLD  9896  aceq0  10118  dfac5  10128  zfac  10459  brdom3  10527  axpowndlem3  10601  zfcndrep  10616  zfcndac  10621  elgch  10624  engch  10630  axgroth3  10833  axgroth4  10834  elnp  10989  elnpi  10990  infm3  12191  fz1sbc  13647  uzrdgfni  14014  trclfvcotr  15072  relexpindlem  15126  vdwmc2  17063  ramtlecl  17084  ramval  17092  ramub  17097  rami  17099  ramcl  17113  mreexexd  17728  mplsubglem  22200  mpllsslem  22201  ismhp3  22357  istopg  23104  1stccn  23673  iskgen3  23759  fbfinnfr  24051  cnextfun  24274  metcld  25518  metcld2  25519  noseqrdgfn  28552  chlimi  31659  nmcexi  32451  disjxun0  32992  disjrdx  33009  axprALT2  35563  tz9.1regs  35606  axsepg5  35616  elkarden  35627  mclsssvlem  36093  mclsval  36094  mclsind  36101  elintfv  36296  dfon2lem6  36317  dfon2lem7  36318  dfon2lem8  36319  dfon2  36321  sscoid  36442  sbequbidv  36785  disjeq12dv  36786  ixpeq12dv  36787  cbvsbdavw  36825  cbvsbdavw2  36826  cbvdisjdavw  36839  cbvdisjdavw2  36860  trer  36886  axtcond  37048  axuntco  37049  regsfromregtco  37108  mh-regprimbi  37115  bj-ssblem1  37335  bj-ax12  37338  mobidvALT  37551  bj-sbceqgALT  37596  bj-inex1gALT  37619  bj-nuliota  37752  bj-bm1.3ii  37759  wl-ax12v2cl  38211  wl-mo2t  38289  findcard4  38424  isass  38557  releccnveq  38970  ecin0  39061  inecmo  39064  alrmomodm  39068  raldmqseu  39074  extssr  39298  eltrrels3  39373  eleqvrels3  39386  axc11n-16  39772  cdlemefrs29bpre0  41230  eu6w  43468  unielss  44005  orddif0suc  44055  elmapintab  44382  cnvcnvintabd  44386  iunrelexpuztr  44505  ntrneiiso  44877  ntrneik2  44878  ntrneix2  44879  ntrneikb  44880  mnuop123d  45032  pm14.122b  45193  iotavalb  45200  trsbc  45309  permaxnul  45777  permaxpow  45778  permaxpr  45779  permaxun  45780  permaxinf2lem  45781  permac8prim  45783  nregmodel  45786  eusnsn  47823  aiota0def  47893  ichbidv  48262  mof0  49675  eufsnlem  49678  termcarweu  50365  setrecseq  50522  setrec1lem1  50524  setrec2fun  50529  setrec2lem2  50531