![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > alimdv | Structured version Unicode version |
Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
alimdv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1671 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | alimdv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | alimdh 1609 |
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-gen 1592 ax-4 1603 ax-5 1671 |
This theorem is referenced by: 2alimdv 1678 axc9lem1 1954 axc16i 2021 morimvOLD 2329 ralimdv2 2898 mo2icl 3238 sstr2 3464 reuss2 3731 ssuni 4214 disjss2 4366 disjss1 4369 disjiun 4383 disjss3 4392 alxfr 4606 frss 4788 ssrel 5029 ssrel2 5031 ssrelrel 5041 iotaval 5493 dff3 5958 dfwe2 6496 ordom 6588 findcard3 7659 dffi2 7777 indcardi 8315 zorn2lem4 8772 uzindi 11913 caubnd 12957 ramtlecl 14172 psgnunilem4 16114 bwthOLD 19139 dfcon2 19148 wilthlem3 22534 nbcusgra 23516 disjss1f 26062 wzel 27898 onsuct0 28424 axc11next 29801 |
Copyright terms: Public domain | W3C validator |