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

Theorem albidv 1915
Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1861 and albid 2217. (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 1905 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2albidh 1861 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wal 1529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905
This theorem depends on definitions:  df-bi 209
This theorem is referenced by:  nfbidv  1917  2albidv  1918  sbjust  2062  sbequ  2084  sb6  2087  ax12wdemo  2133  sb4b  2493  sb4bOLD  2494  mojust  2615  mof  2641  eujust  2650  eujustALT  2651  eu6lem  2652  euf  2655  axextg  2793  axextmo  2795  eqeq1dALT  2822  nfceqdf  2970  drnfc1  2995  drnfc2  2997  ralbidv2  3193  ralxpxfr2d  3637  alexeqg  3642  pm13.183  3657  pm13.183OLD  3658  eqeu  3695  mo2icl  3703  euind  3713  reuind  3742  cdeqal  3758  sbcal  3831  sbcabel  3859  csbiebg  3913  ssconb  4112  reldisj  4400  sbcssg  4461  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  6861  eufnfv  6983  dff13  7005  nfriotadw  7114  tfisi  7565  dfom2  7574  elom  7575  seqomlem2  8079  pssnn  8728  findcard  8749  findcard2  8750  findcard3  8753  fiint  8787  inf0  9076  axinf2  9095  tz9.1  9163  karden  9316  aceq0  9536  dfac5  9546  zfac  9874  brdom3  9942  axpowndlem3  10013  zfcndrep  10028  zfcndac  10033  elgch  10036  engch  10042  axgroth3  10245  axgroth4  10246  elnp  10401  elnpi  10402  infm3  11592  fz1sbc  12975  uzrdgfni  13318  trclfvcotr  14361  relexpindlem  14414  vdwmc2  16307  ramtlecl  16328  ramval  16336  ramub  16341  rami  16343  ramcl  16357  mreexexd  16911  mplsubglem  20206  mpllsslem  20207  istopg  21495  1stccn  22063  iskgen3  22149  fbfinnfr  22441  cnextfun  22664  metcld  23901  metcld2  23902  chlimi  29003  nmcexi  29795  disjxun0  30316  disjrdx  30333  funcnvmpt  30404  mclsssvlem  32802  mclsval  32803  mclsind  32810  elintfv  33000  dfon2lem6  33026  dfon2lem7  33027  dfon2lem8  33028  dfon2  33030  sscoid  33367  trer  33657  bj-ssblem1  33980  bj-ax12  33983  mobidvALT  34174  bj-sbceqgALT  34212  bj-nuliota  34342  bj-bm1.3ii  34349  wl-mo2t  34803  wl-dfralf  34831  isass  35116  releccnveq  35511  ecin0  35598  inecmo  35601  alrmomodm  35605  extssr  35741  eltrrels3  35808  eleqvrels3  35820  axc11n-16  36066  cdlemefrs29bpre0  37524  elmapintab  39947  cnvcnvintabd  39951  iunrelexpuztr  40055  ntrneiiso  40432  ntrneik2  40433  ntrneix2  40434  ntrneikb  40435  mnuop123d  40589  pm14.122b  40746  iotavalb  40753  trsbc  40865  dffo3f  41428  eusnsn  43252  aiota0def  43285  setrecseq  44779  setrec1lem1  44781  setrec2fun  44786  setrec2lem2  44788
  Copyright terms: Public domain W3C validator