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  2480  mojust  2539  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  axextg  2710  axextmo  2712  eqeq1dALT  2740  nfceqdf  2901  drnfc1  2925  drnfc2  2926  ralbidv2  3174  ralxpxfr2d  3646  alexeqg  3651  pm13.183  3666  elab6g  3669  elabd2  3670  eqeu  3712  mo2icl  3720  euind  3730  reuind  3759  cdeqal  3775  sbcal  3849  sbccomlem  3869  sbcabel  3878  csbiebg  3931  ssconb  4142  reldisj  4453  sbcssg  4520  elint  4952  axrep1  5280  axreplem  5281  axrep2  5282  axrep4OLD  5286  zfrepclf  5291  axsepg  5297  zfauscl  5298  bm1.3iiOLD  5302  al0ssb  5308  eusv1  5391  euotd  5518  freq1  5652  frsn  5773  iota5  6544  dffun2  6571  sbcfung  6590  funimass4  6973  dffo3  7122  dffo3f  7126  eufnfv  7249  dff13  7275  fnssintima  7382  nfriotadw  7396  imaeqalov  7672  tfisi  7880  dfom2  7889  elom  7890  xpord3inddlem  8179  seqomlem2  8491  findcard  9203  findcard2  9204  pssnn  9208  ssfi  9213  findcard3  9318  findcard3OLD  9319  fiint  9366  fiintOLD  9367  inf0  9661  axinf2  9680  ttrclss  9760  ttrclselem2  9766  tz9.1  9769  karden  9935  aceq0  10158  dfac5  10169  zfac  10500  brdom3  10568  axpowndlem3  10639  zfcndrep  10654  zfcndac  10659  elgch  10662  engch  10668  axgroth3  10871  axgroth4  10872  elnp  11027  elnpi  11028  infm3  12227  fz1sbc  13640  uzrdgfni  13999  trclfvcotr  15048  relexpindlem  15102  vdwmc2  17017  ramtlecl  17038  ramval  17046  ramub  17051  rami  17053  ramcl  17067  mreexexd  17691  mplsubglem  22019  mpllsslem  22020  ismhp3  22146  istopg  22901  1stccn  23471  iskgen3  23557  fbfinnfr  23849  cnextfun  24072  metcld  25340  metcld2  25341  noseqrdgfn  28312  chlimi  31253  nmcexi  32045  disjxun0  32587  disjrdx  32604  funcnvmpt  32677  mclsssvlem  35567  mclsval  35568  mclsind  35575  elintfv  35765  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon2  35793  sscoid  35914  sbequbidv  36215  disjeq12dv  36216  ixpeq12dv  36217  cbvsbdavw  36255  cbvsbdavw2  36256  cbvdisjdavw  36269  cbvdisjdavw2  36290  trer  36317  bj-ssblem1  36655  bj-ax12  36658  mobidvALT  36858  bj-sbceqgALT  36903  bj-nuliota  37058  bj-bm1.3ii  37065  wl-ax12v2cl  37507  wl-mo2t  37576  isass  37853  releccnveq  38259  ecin0  38353  inecmo  38356  alrmomodm  38360  extssr  38510  eltrrels3  38581  eleqvrels3  38594  axc11n-16  38939  cdlemefrs29bpre0  40398  eu6w  42686  unielss  43230  orddif0suc  43281  elmapintab  43609  cnvcnvintabd  43613  iunrelexpuztr  43732  ntrneiiso  44104  ntrneik2  44105  ntrneix2  44106  ntrneikb  44107  mnuop123d  44281  pm14.122b  44442  iotavalb  44449  trsbc  44560  eusnsn  47038  aiota0def  47108  ichbidv  47440  mof0  48747  eufsnlem  48750  setrecseq  49204  setrec1lem1  49206  setrec2fun  49211  setrec2lem2  49213