Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssopab2i | Structured version Visualization version Unicode version |
Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.) |
Ref | Expression |
---|---|
ssopab2i.1 |
Ref | Expression |
---|---|
ssopab2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssopab2 5001 | . 2 | |
2 | ssopab2i.1 | . . 3 | |
3 | 2 | ax-gen 1722 | . 2 |
4 | 1, 3 | mpg 1724 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wal 1481 wss 3574 copab 4712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-in 3581 df-ss 3588 df-opab 4713 |
This theorem is referenced by: elopabran 5014 opabssxp 5193 funopab4 5925 ssoprab2i 6749 cardf2 8769 dfac3 8944 axdc2lem 9270 fpwwe2lem1 9453 canthwe 9473 trclublem 13734 fullfunc 16566 fthfunc 16567 isfull 16570 isfth 16574 ipoval 17154 ipolerval 17156 eqgfval 17642 2ndcctbss 21258 iscgrg 25407 ishpg 25651 pthsfval 26617 spthsfval 26618 crcts 26683 cycls 26684 eupths 27060 nvss 27448 ajfval 27664 afsval 30749 cvmlift2lem12 31296 opabssi 34130 dicval 36465 areaquad 37802 relopabVD 39137 |
Copyright terms: Public domain | W3C validator |