![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.23v | Structured version Visualization version Unicode version |
Description: Version of 19.23 2004 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) |
Ref | Expression |
---|---|
19.23v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exim 1717 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 19.9v 1823 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6ib 234 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | ax-5 1769 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | imim2i 16 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 19.38 1723 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | syl 17 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | impbii 192 |
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-ex 1675 |
This theorem is referenced by: 19.23vv 1830 pm11.53v 1833 equsalvw 1858 2mo2 2390 euind 3237 reuind 3255 r19.3rzv 3874 unissb 4243 disjor 4401 dftr2 4513 ssrelrel 4954 cotrg 5230 dffun2 5611 fununi 5671 dff13 6184 dffi2 7963 aceq2 8576 psgnunilem4 17187 metcld 22324 metcld2 22325 isch2 26925 disjorf 28238 funcnv5mpt 28321 bnj1052 29833 bnj1030 29845 dfon2lem8 30485 bj-ssbeq 31285 bj-ssb0 31286 bj-ssb1a 31290 bj-ssb1 31291 bj-ssbequ2 31301 bj-ssbid2ALT 31304 elmapintrab 36227 elinintrab 36228 undmrnresiss 36255 elintima 36290 relexp0eq 36338 dfhe3 36415 pm10.52 36758 truniALT 36946 tpid3gVD 37278 truniALTVD 37315 onfrALTVD 37328 unisnALT 37363 |
Copyright terms: Public domain | W3C validator |