MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  albid Unicode version

Theorem albid 1885
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
albid.1
albid.2
Assertion
Ref Expression
albid

Proof of Theorem albid
StepHypRef Expression
1 albid.1 . . 3
21nfri 1874 . 2
3 albid.2 . 2
42, 3albidh 1675 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  F/wnf 1616
This theorem is referenced by:  nfbidf  1887  dral2  2066  dral1  2067  ax12v2  2083  sbal1  2204  sbal2  2205  ax12eq  2271  ax12el  2272  ax12v2-o  2279  eubid  2302  ralbida  2890  raleqf  3050  intab  4317  fin23lem32  8745  axrepndlem1  8988  axrepndlem2  8989  axrepnd  8990  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem4  8998  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  funcnvmptOLD  27509  iota5f  29102  wl-equsald  29992  wl-sbnf1  30003  wl-2sb6d  30008  wl-sbalnae  30012  wl-mo2dnae  30019  wl-ax11-lem6  30030  wl-ax11-lem8  30032  bj-dral1v  34326  bj-axc15v  34330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator