![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ralbidv | Structured version Visualization version Unicode version |
Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.) |
Ref | Expression |
---|---|
2ralbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2ralbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ralbidv 2839 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralbidv 2839 |
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 df-an 377 df-ral 2754 |
This theorem is referenced by: cbvral3v 3041 ralxpxfr2d 3176 poeq1 4777 soeq1 4793 isoeq1 6235 isoeq2 6236 isoeq3 6237 fnmpt2ovd 6898 smoeq 7095 xpf1o 7760 nqereu 9380 dedekind 9823 dedekindle 9824 seqcaopr2 12281 wrd2ind 12871 addcn2 13706 mulcn2 13708 mreexexd 15603 catlid 15638 catrid 15639 isfunc 15818 funcres2b 15851 isfull 15864 isfth 15868 fullres2c 15893 isnat 15901 evlfcl 16156 uncfcurf 16173 isprs 16224 isdrs 16228 ispos 16241 istos 16330 isdlat 16488 sgrp1 16583 ismhm 16633 issubm 16643 sgrp2nmndlem4 16711 isnsg 16895 isghm 16932 isga 16994 pmtrdifwrdel 17175 sylow2blem2 17322 efglem 17415 efgi 17418 efgredlemb 17445 efgred 17447 frgpuplem 17471 iscmn 17486 ring1 17879 isirred 17976 islmod 18144 lmodlema 18145 lssset 18206 islssd 18208 islmhm 18299 islmhm2 18310 isobs 19332 dmatel 19567 dmatmulcl 19574 scmateALT 19586 mdetunilem3 19688 mdetunilem4 19689 mdetunilem9 19694 cpmatel 19784 chpscmat 19915 hausnei2 20418 dfcon2 20483 llyeq 20534 nllyeq 20535 isucn2 21343 iducn 21347 ispsmet 21369 ismet 21387 isxmet 21388 metucn 21635 ngptgp 21693 nlmvscnlem1 21738 xmetdcn2 21904 addcnlem 21945 elcncf 21970 ipcnlem1 22265 cfili 22287 c1lip1 22998 aalioulem5 23341 aalioulem6 23342 aaliou 23343 aaliou2 23345 aaliou2b 23346 ulmcau 23399 ulmdvlem3 23406 cxpcn3lem 23736 dvdsmulf1o 24172 chpdifbndlem2 24441 pntrsumbnd2 24454 istrkgb 24552 axtgsegcon 24561 axtg5seg 24562 axtgpasch 24564 axtgeucl 24569 iscgrg 24606 isismt 24628 isperp2 24809 f1otrg 24950 axcontlem10 25052 axcontlem12 25054 isfrgra 25767 isgrpo 25973 isablo 26060 isass 26093 elghomlem1OLD 26138 elghomlem2OLD 26139 iscom2 26189 vacn 26379 smcnlem 26382 lnoval 26442 islno 26443 isphg 26507 ajmoi 26549 ajval 26552 adjmo 27534 elcnop 27559 ellnop 27560 elunop 27574 elhmop 27575 elcnfn 27584 ellnfn 27585 adjeu 27591 adjval 27592 adj1 27635 adjeq 27637 cnlnadjlem9 27777 cnlnadjeu 27780 cnlnssadj 27782 isst 27915 ishst 27916 cdj1i 28135 cdj3i 28143 resspos 28469 resstos 28470 isomnd 28513 isslmd 28567 slmdlema 28568 isorng 28611 qqhucn 28845 ismntop 28879 axtgupdim2OLD 29534 txpcon 30004 nofulllem4 30643 nofulllem5 30644 nn0prpw 31028 heicant 32020 equivbnd 32167 isismty 32178 heibor1lem 32186 iccbnd 32217 isrngohom 32249 pridlval 32311 ispridl 32312 isdmn3 32352 islfl 32671 isopos 32791 psubspset 33354 islaut 33693 ispautN 33709 ltrnset 33728 isltrn 33729 istrnN 33768 istendo 34372 ismgmhm 40056 issubmgm 40062 isrnghm 40165 lidlmsgrp 40199 lidlrng 40200 dmatALTbasel 40468 lindslinindsimp2 40529 lmod1 40558 |
Copyright terms: Public domain | W3C validator |