![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.42v | Structured version Visualization version Unicode version |
Description: Version of 19.42 2063 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
19.42v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.41v 1841 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | exancom 1733 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | ancom 456 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3bitr4i 285 |
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 ax-6 1816 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 |
This theorem is referenced by: exdistr 1846 19.42vv 1847 19.42vvv 1848 4exdistr 1851 eeeanv 2090 2sb5 2283 rexcom4a 3080 ceqsex2 3098 reuind 3255 2reu5lem3 3259 sbccomlem 3350 bm1.3ii 4544 eqvinop 4703 dmopabss 5068 dmopab3 5069 mptpreima 5351 mptfnf 5725 brprcneu 5885 fndmin 6017 fliftf 6238 dfoprab2 6369 dmoprab 6409 dmoprabss 6410 fnoprabg 6429 uniuni 6632 zfrep6 6793 opabex3d 6803 opabex3 6804 fsplit 6933 eroveu 7489 rankuni 8365 aceq1 8579 dfac3 8583 kmlem14 8624 kmlem15 8625 axdc2lem 8909 1idpr 9485 ltexprlem1 9492 ltexprlem4 9495 xpcogend 13093 shftdm 13189 joindm 16304 meetdm 16318 ntreq0 20148 cnextf 21136 usg2spot2nb 25849 adjeu 27598 rexunirn 28183 fpwrelmapffslem 28369 bnj1019 29641 bnj1209 29658 bnj1033 29828 bnj1189 29868 dfiota3 30740 brimg 30754 funpartlem 30759 bj-eeanvw 31353 bj-rexcom4 31524 bj-rexcom4a 31525 bj-snsetex 31603 bj-snglc 31609 itg2addnc 32042 sbccom2lem 32410 rp-isfinite6 36209 undmrnresiss 36256 elintima 36291 pm11.58 36785 pm11.71 36792 2sbc5g 36812 iotasbc2 36816 ax6e2nd 36970 ax6e2ndVD 37346 ax6e2ndALT 37368 stoweidlem60 38022 |
Copyright terms: Public domain | W3C validator |