New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > albidv | Unicode version |
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
albidv.1 |
Ref | Expression |
---|---|
albidv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1616 | . 2 | |
2 | albidv.1 | . 2 | |
3 | 1, 2 | albidh 1590 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wal 1540 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: 2albidv 1627 ax11wdemo 1723 ax11vALT 2097 sbcom2 2114 ax10-16 2190 eujust 2206 eujustALT 2207 euf 2210 mo 2226 axext3 2336 bm1.1 2338 eqeq1 2359 nfceqdf 2488 ralbidv2 2636 alexeq 2968 pm13.183 2979 eqeu 3007 mo2icl 3015 euind 3023 reuind 3039 sbcal 3093 sbcalg 3094 sbcabel 3123 csbiebg 3175 ssconb 3399 reldisj 3594 sbcss 3660 elint 3932 iota5 4359 nnadjoin 4520 sfintfin 4532 tfinnn 4534 spfinsfincl 4539 spfininduct 4540 ssrel 4844 funimass4 5368 dffo3 5422 dff13 5471 fnfullfunlem1 5856 frd 5922 |
Copyright terms: Public domain | W3C validator |