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  32611  tz9.1regs  35073  mclsssvlem  35545  mclsval  35546  mclsind  35553  elintfv  35748  dfon2lem6  35772  dfon2lem7  35773  dfon2lem8  35774  dfon2  35776  sscoid  35897  sbequbidv  36198  disjeq12dv  36199  ixpeq12dv  36200  cbvsbdavw  36238  cbvsbdavw2  36239  cbvdisjdavw  36252  cbvdisjdavw2  36273  trer  36300  bj-ssblem1  36638  bj-ax12  36641  mobidvALT  36841  bj-sbceqgALT  36886  bj-nuliota  37041  bj-bm1.3ii  37048  wl-ax12v2cl  37490  wl-mo2t  37559  isass  37836  releccnveq  38243  ecin0  38330  inecmo  38333  alrmomodm  38337  extssr  38496  eltrrels3  38567  eleqvrels3  38580  axc11n-16  38927  cdlemefrs29bpre0  40385  eu6w  42659  unielss  43201  orddif0suc  43251  elmapintab  43579  cnvcnvintabd  43583  iunrelexpuztr  43702  ntrneiiso  44074  ntrneik2  44075  ntrneix2  44076  ntrneikb  44077  mnuop123d  44245  pm14.122b  44406  iotavalb  44413  trsbc  44524  permaxnul  44992  permaxpow  44993  permaxpr  44994  permaxun  44995  permaxinf2lem  44996  permac8prim  44998  nregmodel  45001  eusnsn  47020  aiota0def  47090  ichbidv  47447  mof0  48832  eufsnlem  48835  termcarweu  49523  setrecseq  49680  setrec1lem1  49682  setrec2fun  49687  setrec2lem2  49689