MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  albidv Structured version   Visualization version   GIF version

Theorem albidv 1912
Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1858 and albid 2214. (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
StepHypRef Expression
1 ax-5 1902 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2albidh 1858 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  nfbidv  1914  2albidv  1915  sbjust  2059  sbequ  2081  sb6  2084  ax12wdemo  2130  sb4b  2492  sb4bOLD  2493  mojust  2614  mof  2640  eujust  2649  eujustALT  2650  eu6lem  2651  euf  2654  axextg  2792  axextmo  2794  eqeq1dALT  2821  nfceqdf  2969  drnfc1  2994  drnfc2  2996  ralbidv2  3192  ralxpxfr2d  3636  alexeqg  3641  pm13.183  3656  pm13.183OLD  3657  eqeu  3694  mo2icl  3702  euind  3712  reuind  3741  cdeqal  3757  sbcal  3830  sbcabel  3858  csbiebg  3912  ssconb  4111  reldisj  4398  sbcssg  4459  elint  4873  axrep1  5182  axreplem  5183  axrep2  5184  axrep4  5186  zfrepclf  5189  axsepg  5195  zfauscl  5196  bm1.3ii  5197  al0ssb  5203  eusv1  5282  euotd  5394  freq1  5518  frsn  5632  iota5  6331  sbcfung  6372  funimass4  6723  dffo3  6860  eufnfv  6982  dff13  7004  nfriotadw  7111  tfisi  7562  dfom2  7571  elom  7572  seqomlem2  8076  pssnn  8724  findcard  8745  findcard2  8746  findcard3  8749  fiint  8783  inf0  9072  axinf2  9091  tz9.1  9159  karden  9312  aceq0  9532  dfac5  9542  zfac  9870  brdom3  9938  axpowndlem3  10009  zfcndrep  10024  zfcndac  10029  elgch  10032  engch  10038  axgroth3  10241  axgroth4  10242  elnp  10397  elnpi  10398  infm3  11588  fz1sbc  12971  uzrdgfni  13314  trclfvcotr  14357  relexpindlem  14410  vdwmc2  16303  ramtlecl  16324  ramval  16332  ramub  16337  rami  16339  ramcl  16353  mreexexd  16907  mplsubglem  20142  mpllsslem  20143  istopg  21431  1stccn  21999  iskgen3  22085  fbfinnfr  22377  cnextfun  22600  metcld  23836  metcld2  23837  chlimi  28938  nmcexi  29730  disjxun0  30252  disjrdx  30269  funcnvmpt  30340  mclsssvlem  32706  mclsval  32707  mclsind  32714  elintfv  32904  dfon2lem6  32930  dfon2lem7  32931  dfon2lem8  32932  dfon2  32934  sscoid  33271  trer  33561  bj-ssblem1  33884  bj-ax12  33887  mobidvALT  34078  bj-sbceqgALT  34116  bj-nuliota  34244  bj-bm1.3ii  34251  wl-mo2t  34692  wl-dfralf  34720  isass  35005  releccnveq  35400  ecin0  35487  inecmo  35490  alrmomodm  35494  extssr  35629  eltrrels3  35696  eleqvrels3  35708  axc11n-16  35954  cdlemefrs29bpre0  37412  elmapintab  39834  cnvcnvintabd  39838  iunrelexpuztr  39942  ntrneiiso  40319  ntrneik2  40320  ntrneix2  40321  ntrneikb  40322  mnuop123d  40475  pm14.122b  40632  iotavalb  40639  trsbc  40751  dffo3f  41314  eusnsn  43138  aiota0def  43171  setrecseq  44716  setrec1lem1  44718  setrec2fun  44723  setrec2lem2  44725
  Copyright terms: Public domain W3C validator