![]() |
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 4727 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssopab2i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | ax-gen 1669 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpg 1671 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-in 3411 df-ss 3418 df-opab 4462 |
This theorem is referenced by: brab2a 4884 opabssxp 4909 funopab4 5617 ssoprab2i 6385 cardf2 8377 dfac3 8552 axdc2lem 8878 fpwwe2lem1 9056 canthwe 9076 trclublem 13059 fullfunc 15811 fthfunc 15812 isfull 15815 isfth 15819 ipoval 16400 ipolerval 16402 eqgfval 16865 2ndcctbss 20470 iscgrg 24557 ishpg 24801 nvss 26212 ajfval 26450 afsval 29488 cvmlift2lem12 30037 dicval 34744 areaquad 36101 relopabVD 37298 |
Copyright terms: Public domain | W3C validator |