![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > albid | Structured version Unicode version |
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
albid.1 |
![]() ![]() ![]() ![]() |
albid.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
albid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albid.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | nfri 1810 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | albid.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | albidh 1643 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-12 1794 |
This theorem depends on definitions: df-bi 185 df-ex 1588 df-nf 1591 |
This theorem is referenced by: nfbidf 1823 dral2 2023 dral1 2024 ax12v2 2040 sbal1 2178 sbal2 2180 sbal2OLD 2191 ax12eq 2249 ax12el 2250 ax12v2-o 2257 eubid 2281 ralbidaOLD 2834 raleqf 3011 intab 4258 fin23lem32 8616 axrepndlem1 8859 axrepndlem2 8860 axrepnd 8861 axunnd 8863 axpowndlem2 8865 axpowndlem2OLD 8866 axpowndlem4 8869 axregndlem2 8872 axinfndlem1 8875 axinfnd 8876 axacndlem4 8880 axacndlem5 8881 axacnd 8882 funcnvmptOLD 26122 iota5f 27517 wl-equsald 28508 wl-sbnf1 28519 wl-2sb6d 28524 wl-sbalnae 28528 wl-mo2dnae 28535 wl-ax11-lem6 28546 wl-ax11-lem8 28548 bj-dral1v 32563 bj-axc15v 32567 |
Copyright terms: Public domain | W3C validator |