Theorem albidv 1920

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  nfbidv  1922  2albidv  1923  sbjust  2064  sbequ  2084  sb6  2086  ax12wdemo  2136  sb4b  2474  mojust  2533  mof  2557  eujust  2565  eujustALT  2566  eu6lem  2567  euf  2570  axextg  2704  axextmo  2706  eqeq1dALT  2733  nfceqdf  2888  drnfc1  2912  drnfc2  2913  ralbidv2  3153  ralxpxfr2d  3615  alexeqg  3620  pm13.183  3635  elab6g  3638  elabd2  3639  eqeu  3680  mo2icl  3688  euind  3698  reuind  3727  cdeqal  3743  sbcal  3816  sbccomlem  3835  sbcabel  3844  csbiebg  3897  ssconb  4108  reldisj  4419  sbcssg  4486  elint  4919  axrep1  5238  axreplem  5239  axrep2  5240  axrep4OLD  5244  zfrepclf  5249  axsepg  5255  zfauscl  5256  bm1.3iiOLD  5260  al0ssb  5266  eusv1  5349  euotd  5476  freq1  5608  frsn  5729  iota5  6497  dffun2  6524  sbcfung  6543  funimass4  6928  dffo3  7077  dffo3f  7081  eufnfv  7206  dff13  7232  fnssintima  7340  nfriotadw  7355  imaeqalov  7631  tfisi  7838  dfom2  7847  elom  7848  xpord3inddlem  8136  seqomlem2  8422  findcard  9133  findcard2  9134  pssnn  9138  ssfi  9143  findcard3  9236  findcard3OLD  9237  fiint  9284  fiintOLD  9285  inf0  9581  axinf2  9600  ttrclss  9680  ttrclselem2  9686  tz9.1  9689  karden  9855  aceq0  10078  dfac5  10089  zfac  10420  brdom3  10488  axpowndlem3  10559  zfcndrep  10574  zfcndac  10579  elgch  10582  engch  10588  axgroth3  10791  axgroth4  10792  elnp  10947  elnpi  10948  infm3  12149  fz1sbc  13568  uzrdgfni  13930  trclfvcotr  14982  relexpindlem  15036  vdwmc2  16957  ramtlecl  16978  ramval  16986  ramub  16991  rami  16993  ramcl  17007  mreexexd  17616  mplsubglem  21915  mpllsslem  21916  ismhp3  22036  istopg  22789  1stccn  23357  iskgen3  23443  fbfinnfr  23735  cnextfun  23958  metcld  25213  metcld2  25214  noseqrdgfn  28207  chlimi  31170  nmcexi  31962  disjxun0  32510  disjrdx  32527  funcnvmpt  32598  mclsssvlem  35556  mclsval  35557  mclsind  35564  elintfv  35759  dfon2lem6  35783  dfon2lem7  35784  dfon2lem8  35785  dfon2  35787  sscoid  35908  sbequbidv  36209  disjeq12dv  36210  ixpeq12dv  36211  cbvsbdavw  36249  cbvsbdavw2  36250  cbvdisjdavw  36263  cbvdisjdavw2  36284  trer  36311  bj-ssblem1  36649  bj-ax12  36652  mobidvALT  36852  bj-sbceqgALT  36897  bj-nuliota  37052  bj-bm1.3ii  37059  wl-ax12v2cl  37501  wl-mo2t  37570  isass  37847  releccnveq  38254  ecin0  38341  inecmo  38344  alrmomodm  38348  extssr  38507  eltrrels3  38578  eleqvrels3  38591  axc11n-16  38938  cdlemefrs29bpre0  40397  eu6w  42671  unielss  43214  orddif0suc  43264  elmapintab  43592  cnvcnvintabd  43596  iunrelexpuztr  43715  ntrneiiso  44087  ntrneik2  44088  ntrneix2  44089  ntrneikb  44090  mnuop123d  44258  pm14.122b  44419  iotavalb  44426  trsbc  44537  permaxnul  45005  permaxpow  45006  permaxpr  45007  permaxun  45008  permaxinf2lem  45009  permac8prim  45011  nregmodel  45014  eusnsn  47031  aiota0def  47101  ichbidv  47458  mof0  48830  eufsnlem  48833  termcarweu  49521  setrecseq  49678  setrec1lem1  49680  setrec2fun  49685  setrec2lem2  49687