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  3148  ralxpxfr2d  3601  alexeqg  3606  pm13.183  3621  elab6g  3624  elabd2  3625  eqeu  3666  mo2icl  3674  euind  3684  reuind  3713  cdeqal  3729  sbcal  3802  sbccomlem  3821  sbcabel  3830  csbiebg  3883  ssconb  4093  reldisj  4404  sbcssg  4471  elint  4902  axrep1  5219  axreplem  5220  axrep2  5221  axrep4OLD  5225  zfrepclf  5230  axsepg  5236  zfauscl  5237  bm1.3iiOLD  5241  al0ssb  5247  eusv1  5330  euotd  5456  freq1  5586  frsn  5707  iota5  6465  dffun2  6492  sbcfung  6506  funimass4  6887  dffo3  7036  dffo3f  7040  eufnfv  7165  dff13  7191  fnssintima  7299  nfriotadw  7314  imaeqalov  7588  tfisi  7792  dfom2  7801  elom  7802  xpord3inddlem  8087  seqomlem2  8373  findcard  9077  findcard2  9078  pssnn  9082  ssfi  9087  findcard3  9172  fiint  9216  fiintOLD  9217  inf0  9517  axinf2  9536  ttrclss  9616  ttrclselem2  9622  tz9.1  9625  karden  9791  aceq0  10012  dfac5  10023  zfac  10354  brdom3  10422  axpowndlem3  10493  zfcndrep  10508  zfcndac  10513  elgch  10516  engch  10522  axgroth3  10725  axgroth4  10726  elnp  10881  elnpi  10882  infm3  12084  fz1sbc  13503  uzrdgfni  13865  trclfvcotr  14916  relexpindlem  14970  vdwmc2  16891  ramtlecl  16912  ramval  16920  ramub  16925  rami  16927  ramcl  16941  mreexexd  17554  mplsubglem  21906  mpllsslem  21907  ismhp3  22027  istopg  22780  1stccn  23348  iskgen3  23434  fbfinnfr  23726  cnextfun  23949  metcld  25204  metcld2  25205  noseqrdgfn  28205  chlimi  31178  nmcexi  31970  disjxun0  32518  disjrdx  32535  funcnvmpt  32610  tz9.1regs  35067  mclsssvlem  35535  mclsval  35536  mclsind  35543  elintfv  35738  dfon2lem6  35762  dfon2lem7  35763  dfon2lem8  35764  dfon2  35766  sscoid  35887  sbequbidv  36188  disjeq12dv  36189  ixpeq12dv  36190  cbvsbdavw  36228  cbvsbdavw2  36229  cbvdisjdavw  36242  cbvdisjdavw2  36263  trer  36290  bj-ssblem1  36628  bj-ax12  36631  mobidvALT  36831  bj-sbceqgALT  36876  bj-nuliota  37031  bj-bm1.3ii  37038  wl-ax12v2cl  37480  wl-mo2t  37549  isass  37826  releccnveq  38233  ecin0  38320  inecmo  38323  alrmomodm  38327  extssr  38486  eltrrels3  38557  eleqvrels3  38570  axc11n-16  38917  cdlemefrs29bpre0  40375  eu6w  42649  unielss  43191  orddif0suc  43241  elmapintab  43569  cnvcnvintabd  43573  iunrelexpuztr  43692  ntrneiiso  44064  ntrneik2  44065  ntrneix2  44066  ntrneikb  44067  mnuop123d  44235  pm14.122b  44396  iotavalb  44403  trsbc  44514  permaxnul  44982  permaxpow  44983  permaxpr  44984  permaxun  44985  permaxinf2lem  44986  permac8prim  44988  nregmodel  44991  eusnsn  47010  aiota0def  47080  ichbidv  47437  mof0  48822  eufsnlem  48825  termcarweu  49513  setrecseq  49670  setrec1lem1  49672  setrec2fun  49677  setrec2lem2  49679