![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssopab2i | Structured version Visualization version GIF 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 5139 | . 2 ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) | |
2 | ssopab2i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 2 | ax-gen 1859 | . 2 ⊢ ∀𝑦(𝜑 → 𝜓) |
4 | 1, 3 | mpg 1861 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1618 ⊆ wss 3703 {copab 4852 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-in 3710 df-ss 3717 df-opab 4853 |
This theorem is referenced by: elopabran 5152 opabssxp 5338 funopab4 6074 ssoprab2i 6902 cnvoprab 7385 cardf2 8930 dfac3 9105 axdc2lem 9433 fpwwe2lem1 9616 canthwe 9636 trclublem 13906 fullfunc 16738 fthfunc 16739 isfull 16742 isfth 16746 ipoval 17326 ipolerval 17328 eqgfval 17814 2ndcctbss 21431 iscgrg 25577 ishpg 25821 pthsfval 26798 spthsfval 26799 crcts 26865 cycls 26866 eupths 27323 nvss 27728 ajfval 27944 afsval 31029 cvmlift2lem12 31574 dicval 36936 areaquad 38273 relopabVD 39605 |
Copyright terms: Public domain | W3C validator |