![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralcom4 | Structured version Visualization version Unicode version |
Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Ref | Expression |
---|---|
ralcom4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralcom 2953 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ralv 3063 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | ralbii 2821 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | ralv 3063 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 3, 4 | 3bitr3i 279 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ral 2744 df-v 3049 |
This theorem is referenced by: ralxpxfr2d 3166 uniiunlem 3519 iunss 4322 disjor 4390 trint 4515 reliun 4957 funimass4 5921 ralrnmpt2 6416 findcard3 7819 kmlem12 8596 fimaxre3 10560 vdwmc2 14941 ramtlecl 14963 iunocv 19256 1stccn 20490 itg2leub 22704 mptelee 24937 nmoubi 26425 nmopub 27573 nmfnleub 27590 moel 28131 disjorf 28201 funcnv5mpt 28284 untuni 30348 heibor1lem 32153 pmapglbx 33346 ss2iundf 36263 |
Copyright terms: Public domain | W3C validator |