Theorem albidv 1920

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1866 and albid 2222. (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  2063  sbequ  2083  sb6  2085  ax12wdemo  2135  sb4b  2479  mojust  2538  mof  2562  eujust  2570  eujustALT  2571  eu6lem  2572  euf  2575  axextg  2709  axextmo  2711  eqeq1dALT  2738  nfceqdf  2894  drnfc1  2918  drnfc2  2919  ralbidv2  3159  ralxpxfr2d  3625  alexeqg  3630  pm13.183  3645  elab6g  3648  elabd2  3649  eqeu  3689  mo2icl  3697  euind  3707  reuind  3736  cdeqal  3752  sbcal  3825  sbccomlem  3844  sbcabel  3853  csbiebg  3906  ssconb  4117  reldisj  4428  sbcssg  4495  elint  4928  axrep1  5250  axreplem  5251  axrep2  5252  axrep4OLD  5256  zfrepclf  5261  axsepg  5267  zfauscl  5268  bm1.3iiOLD  5272  al0ssb  5278  eusv1  5361  euotd  5488  freq1  5621  frsn  5742  iota5  6514  dffun2  6541  sbcfung  6560  funimass4  6943  dffo3  7092  dffo3f  7096  eufnfv  7221  dff13  7247  fnssintima  7355  nfriotadw  7370  imaeqalov  7646  tfisi  7854  dfom2  7863  elom  7864  xpord3inddlem  8153  seqomlem2  8465  findcard  9177  findcard2  9178  pssnn  9182  ssfi  9187  findcard3  9290  findcard3OLD  9291  fiint  9338  fiintOLD  9339  inf0  9635  axinf2  9654  ttrclss  9734  ttrclselem2  9740  tz9.1  9743  karden  9909  aceq0  10132  dfac5  10143  zfac  10474  brdom3  10542  axpowndlem3  10613  zfcndrep  10628  zfcndac  10633  elgch  10636  engch  10642  axgroth3  10845  axgroth4  10846  elnp  11001  elnpi  11002  infm3  12201  fz1sbc  13617  uzrdgfni  13976  trclfvcotr  15028  relexpindlem  15082  vdwmc2  16999  ramtlecl  17020  ramval  17028  ramub  17033  rami  17035  ramcl  17049  mreexexd  17660  mplsubglem  21959  mpllsslem  21960  ismhp3  22080  istopg  22833  1stccn  23401  iskgen3  23487  fbfinnfr  23779  cnextfun  24002  metcld  25258  metcld2  25259  noseqrdgfn  28252  chlimi  31215  nmcexi  32007  disjxun0  32555  disjrdx  32572  funcnvmpt  32645  mclsssvlem  35584  mclsval  35585  mclsind  35592  elintfv  35782  dfon2lem6  35806  dfon2lem7  35807  dfon2lem8  35808  dfon2  35810  sscoid  35931  sbequbidv  36232  disjeq12dv  36233  ixpeq12dv  36234  cbvsbdavw  36272  cbvsbdavw2  36273  cbvdisjdavw  36286  cbvdisjdavw2  36307  trer  36334  bj-ssblem1  36672  bj-ax12  36675  mobidvALT  36875  bj-sbceqgALT  36920  bj-nuliota  37075  bj-bm1.3ii  37082  wl-ax12v2cl  37524  wl-mo2t  37593  isass  37870  releccnveq  38276  ecin0  38370  inecmo  38373  alrmomodm  38377  extssr  38527  eltrrels3  38598  eleqvrels3  38611  axc11n-16  38956  cdlemefrs29bpre0  40415  eu6w  42699  unielss  43242  orddif0suc  43292  elmapintab  43620  cnvcnvintabd  43624  iunrelexpuztr  43743  ntrneiiso  44115  ntrneik2  44116  ntrneix2  44117  ntrneikb  44118  mnuop123d  44286  pm14.122b  44447  iotavalb  44454  trsbc  44565  permaxnul  45033  permaxpow  45034  permaxpr  45035  permaxun  45036  permaxinf2lem  45037  eusnsn  47055  aiota0def  47125  ichbidv  47467  mof0  48816  eufsnlem  48819  termcarweu  49413  setrecseq  49549  setrec1lem1  49551  setrec2fun  49556  setrec2lem2  49558