| 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 1317 |
. 2
| |
| 2 | 1 | 19.41 1448 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: 19.41vv 1686 19.41vvv 1687 eeeanv 1708 eeeanvOLD 1709 gencbvex 2334 gencbvexOLD 2335 euxfr 2438 euind 2439 sbcgfOLD 2521 iunconstOLD 3263 zfpair 3522 opabidOLD 3558 opabn0 3575 opelxpOLD 4037 relop 4113 dmuni 4166 dmres 4234 rnuni 4327 dminss 4330 imainss 4331 ssrnres 4354 resco 4402 rnco 4404 coass 4415 f11o 4666 imaiun 4840 rnoprab 4933 domen 5438 xpassen 5500 kmlem3 5929 cflem 6053 prnmadd 6252 genpass 6264 ltexprlem4 6297 reclem1pr 6308 reclem2pr 6309 suplem1pr 6313 elreal 6402 infcvglem1 8482 extbas1 10291 bnj512 12519 bnj534 12531 bnj851 12786 bnj903 12819 bnj607 13304 bnj908 13329 bnj986 13360 dftr6 13834 frxp 13951 19.41vvvv 14271 eeeeanv 14272 cnvresima 15359 prter2 16285 prter3 16286 pm11.6 16349 pm11.71 16354 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 1305 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 |
| This theorem depends on definitions: df-bi 164 df-an 242 df-ex 1327 |