Theorem albidv 1950

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1896 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 1940	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1896	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 1825  ax-4 1839  ax-5 1940

This proof depends on definitions:  df-bi 210

This theorem is used by:  nfbidv  1952  2albidv  1953  sbjust  2095  sbequ  2117  sb6  2119  ax12wdemo  2170  sb4b  2507  mojust  2566  mof  2591  eujust  2599  eujustALT  2600  eu6lem  2601  euf  2604  axextg  2737  axextmo  2739  eqeq1dALT  2766  nfceqdf  2921  drnfc1  2944  drnfc2  2945  ralbidv2  3184  ralxpxfr2d  3605  alexeqg  3610  pm13.183  3625  elab6g  3628  elabd2  3629  eqeu  3669  mo2icl  3677  euind  3687  reuind  3716  cdeqal  3732  sbcal  3803  sbccomlem  3822  sbcabel  3831  csbiebg  3885  ssconb  4096  reldisj  4413  sbcssg  4482  elint  4918  axrep1  5239  axreplem  5240  axrep2  5241  axrep4OLD  5245  zfrepclf  5252  axsepg  5258  sepg  5259  zfausclOLD  5261  bm1.3iiOLD  5265  al0ssb  5271  eusv1  5362  euotd  5496  freq1  5628  frsn  5749  iota5  6519  dffun2  6546  sbcfung  6560  funimass4  6945  funcnvmpt  6991  dffo3  7097  dffo3f  7101  eufnfv  7227  dff13  7252  fnssintima  7360  nfriotadw  7375  imaeqalov  7649  tfisi  7851  dfom2  7860  elom  7861  xpord3inddlem  8146  seqomlem2  8434  findcard  9144  findcard2  9145  pssnn  9149  ssfi  9153  findcard3  9239  fiint  9282  elirrv  9555  inf0  9586  axinf2  9605  ttrclss  9685  ttrclselem2  9691  tz9.1  9694  kardenOLD  9885  aceq0  10107  dfac5  10117  zfac  10448  brdom3  10516  axpowndlem3  10588  zfcndrep  10603  zfcndac  10608  elgch  10611  engch  10617  axgroth3  10820  axgroth4  10821  elnp  10976  elnpi  10977  infm3  12178  fz1sbc  13633  uzrdgfni  13999  trclfvcotr  15051  relexpindlem  15105  vdwmc2  17043  ramtlecl  17064  ramval  17072  ramub  17077  rami  17079  ramcl  17093  mreexexd  17708  mplsubglem  22157  mpllsslem  22158  ismhp3  22314  istopg  23061  1stccn  23629  iskgen3  23715  fbfinnfr  24007  cnextfun  24230  metcld  25474  metcld2  25475  noseqrdgfn  28508  chlimi  31595  nmcexi  32387  disjxun0  32928  disjrdx  32945  axprALT2  35512  tz9.1regs  35555  axsepg5  35565  elkarden  35576  mclsssvlem  36062  mclsval  36063  mclsind  36070  elintfv  36265  dfon2lem6  36286  dfon2lem7  36287  dfon2lem8  36288  dfon2  36290  sscoid  36411  sbequbidv  36754  disjeq12dv  36755  ixpeq12dv  36756  cbvsbdavw  36794  cbvsbdavw2  36795  cbvdisjdavw  36808  cbvdisjdavw2  36829  trer  36855  axtcond  37017  axuntco  37018  regsfromregtco  37077  mh-regprimbi  37084  bj-ssblem1  37304  bj-ax12  37307  mobidvALT  37520  bj-sbceqgALT  37565  bj-inex1gALT  37588  bj-nuliota  37721  bj-bm1.3ii  37728  wl-ax12v2cl  38180  wl-mo2t  38258  isass  38525  releccnveq  38938  ecin0  39029  inecmo  39032  alrmomodm  39036  raldmqseu  39042  extssr  39266  eltrrels3  39341  eleqvrels3  39354  axc11n-16  39740  cdlemefrs29bpre0  41198  eu6w  43436  unielss  43973  orddif0suc  44023  elmapintab  44350  cnvcnvintabd  44354  iunrelexpuztr  44473  ntrneiiso  44845  ntrneik2  44846  ntrneix2  44847  ntrneikb  44848  mnuop123d  45000  pm14.122b  45161  iotavalb  45168  trsbc  45277  permaxnul  45745  permaxpow  45746  permaxpr  45747  permaxun  45748  permaxinf2lem  45749  permac8prim  45751  nregmodel  45754  eusnsn  47791  aiota0def  47861  ichbidv  48230  mof0  49644  eufsnlem  49647  termcarweu  50334  setrecseq  50491  setrec1lem1  50493  setrec2fun  50498  setrec2lem2  50500