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  2473  mojust  2532  mof  2556  eujust  2564  eujustALT  2565  eu6lem  2566  euf  2569  axextg  2703  axextmo  2705  eqeq1dALT  2732  nfceqdf  2887  drnfc1  2911  drnfc2  2912  ralbidv2  3152  ralxpxfr2d  3612  alexeqg  3617  pm13.183  3632  elab6g  3635  elabd2  3636  eqeu  3677  mo2icl  3685  euind  3695  reuind  3724  cdeqal  3740  sbcal  3813  sbccomlem  3832  sbcabel  3841  csbiebg  3894  ssconb  4105  reldisj  4416  sbcssg  4483  elint  4916  axrep1  5235  axreplem  5236  axrep2  5237  axrep4OLD  5241  zfrepclf  5246  axsepg  5252  zfauscl  5253  bm1.3iiOLD  5257  al0ssb  5263  eusv1  5346  euotd  5473  freq1  5605  frsn  5726  iota5  6494  dffun2  6521  sbcfung  6540  funimass4  6925  dffo3  7074  dffo3f  7078  eufnfv  7203  dff13  7229  fnssintima  7337  nfriotadw  7352  imaeqalov  7628  tfisi  7835  dfom2  7844  elom  7845  xpord3inddlem  8133  seqomlem2  8419  findcard  9127  findcard2  9128  pssnn  9132  ssfi  9137  findcard3  9229  findcard3OLD  9230  fiint  9277  fiintOLD  9278  inf0  9574  axinf2  9593  ttrclss  9673  ttrclselem2  9679  tz9.1  9682  karden  9848  aceq0  10071  dfac5  10082  zfac  10413  brdom3  10481  axpowndlem3  10552  zfcndrep  10567  zfcndac  10572  elgch  10575  engch  10581  axgroth3  10784  axgroth4  10785  elnp  10940  elnpi  10941  infm3  12142  fz1sbc  13561  uzrdgfni  13923  trclfvcotr  14975  relexpindlem  15029  vdwmc2  16950  ramtlecl  16971  ramval  16979  ramub  16984  rami  16986  ramcl  17000  mreexexd  17609  mplsubglem  21908  mpllsslem  21909  ismhp3  22029  istopg  22782  1stccn  23350  iskgen3  23436  fbfinnfr  23728  cnextfun  23951  metcld  25206  metcld2  25207  noseqrdgfn  28200  chlimi  31163  nmcexi  31955  disjxun0  32503  disjrdx  32520  funcnvmpt  32591  mclsssvlem  35549  mclsval  35550  mclsind  35557  elintfv  35752  dfon2lem6  35776  dfon2lem7  35777  dfon2lem8  35778  dfon2  35780  sscoid  35901  sbequbidv  36202  disjeq12dv  36203  ixpeq12dv  36204  cbvsbdavw  36242  cbvsbdavw2  36243  cbvdisjdavw  36256  cbvdisjdavw2  36277  trer  36304  bj-ssblem1  36642  bj-ax12  36645  mobidvALT  36845  bj-sbceqgALT  36890  bj-nuliota  37045  bj-bm1.3ii  37052  wl-ax12v2cl  37494  wl-mo2t  37563  isass  37840  releccnveq  38247  ecin0  38334  inecmo  38337  alrmomodm  38341  extssr  38500  eltrrels3  38571  eleqvrels3  38584  axc11n-16  38931  cdlemefrs29bpre0  40390  eu6w  42664  unielss  43207  orddif0suc  43257  elmapintab  43585  cnvcnvintabd  43589  iunrelexpuztr  43708  ntrneiiso  44080  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  mnuop123d  44251  pm14.122b  44412  iotavalb  44419  trsbc  44530  permaxnul  44998  permaxpow  44999  permaxpr  45000  permaxun  45001  permaxinf2lem  45002  permac8prim  45004  nregmodel  45007  eusnsn  47027  aiota0def  47097  ichbidv  47454  mof0  48826  eufsnlem  48829  termcarweu  49517  setrecseq  49674  setrec1lem1  49676  setrec2fun  49681  setrec2lem2  49683