| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Special case of Theorem 19.41 of [Margaris] p. 90. |
| Ref | Expression |
|---|---|
| 19.41v |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-17 1012 |
. 2
| |
| 2 | 1 | 19.41 1136 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: 19.41vv 1348 19.41vvv 1349 eeeanv 1366 r19.41v 1810 gencbvex 1885 euxfr 1974 sbcgf 2036 iunconst 2626 zfpair 2833 opabid 2866 opabn0 2880 opelxp 3271 relop 3332 dmuni 3376 dmres 3437 rnuni 3516 dminss 3519 imainss 3520 ssrnres 3538 resco 3557 rnco 3559 coass 3569 f11o 3769 imaiun 3921 rnoprab 4062 domen 4440 xpassen 4504 kmlem3 4829 cflem 4970 prnmadd 5165 genpass 5177 ltexprlem4 5210 reclem1pr 5221 reclem2pr 5222 suplem1pr 5226 elreal 5315 infcvglem1 7311 19.41vvvv 10521 eeeeanv 10522 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 1004 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 |
| This theorem depends on definitions: df-bi 154 df-or 231 df-an 232 df-ex 1022 |