![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > albidv | Structured version Visualization version Unicode version |
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
albidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
albidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1769 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | albidv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | albidh 1737 |
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 1680 ax-4 1693 ax-5 1769 |
This theorem depends on definitions: df-bi 190 |
This theorem is referenced by: 2albidv 1780 ax12wdemo 1920 eujust 2312 eujustALT 2313 euf 2318 mo2 2319 axext3 2444 axext3ALT 2445 bm1.1 2447 eqeq1dALT 2465 nfceqdf 2599 ralbidv2 2835 ralxpxfr2d 3176 alexeqg 3180 pm13.183 3191 eqeu 3221 mo2icl 3229 euind 3237 reuind 3255 cdeqal 3268 sbcal 3329 sbcabel 3357 csbiebg 3398 ssconb 3578 reldisj 3820 sbcssg 3892 elint 4254 axrep1 4530 axrep2 4531 axrep3 4532 axrep4 4533 zfrepclf 4535 axsep2 4540 zfauscl 4541 bm1.3ii 4542 eusv1 4611 euotd 4716 freq1 4823 frsn 4924 iota5 5585 sbcfung 5624 funimass4 5939 dffo3 6060 eufnfv 6164 dff13 6184 tfisi 6712 dfom2 6721 elom 6722 seqomlem2 7194 pssnn 7816 findcard 7836 findcard2 7837 findcard3 7840 fiint 7874 inf0 8152 axinf2 8171 tz9.1 8239 karden 8392 aceq0 8575 dfac5 8585 zfac 8916 brdom3 8982 axpowndlem3 9050 zfcndrep 9065 zfcndac 9070 elgch 9073 engch 9079 axgroth3 9282 axgroth4 9283 elnp 9438 elnpi 9439 infm3 10596 fz1sbc 11899 uzrdgfni 12204 trclfvcotr 13122 relexpindlem 13175 vdwmc2 14978 ramtlecl 15000 ramval 15009 ramvalOLD 15010 ramub 15019 rami 15021 ramcl 15036 mreexexd 15603 mplsubglem 18707 mpllsslem 18708 istopg 19974 1stccn 20527 iskgen3 20613 fbfinnfr 20905 cnextfun 21128 metcld 22324 metcld2 22325 cusgrauvtxb 25273 isass 26093 chlimi 26936 nmcexi 27728 disjrdx 28250 funcnvmpt 28320 mclsssvlem 30249 mclsval 30250 mclsind 30257 dfon2lem6 30483 dfon2lem7 30484 dfon2lem8 30485 dfon2 30487 sscoid 30729 trer 31021 bj-ssbequ 31287 bj-ssblem1 31288 bj-axext3 31429 bj-axrep1 31448 bj-axrep2 31449 bj-axrep3 31450 bj-axrep4 31451 bj-sbceqgALT 31549 bj-axsep2 31573 bj-nuliota 31668 wl-mo2t 31949 axc11n-16 32554 cdlemefrs29bpre0 34008 elmapintab 36247 cnvcnvintabd 36251 iunrelexpuztr 36356 pm14.122b 36818 iotavalb 36825 trsbc 36945 sbcalgOLD 36947 dffo3f 37488 fun2dmnopgexmpl 39070 |
Copyright terms: Public domain | W3C validator |