![]() |
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 5134 | . 2 ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) | |
2 | ssopab2i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 2 | ax-gen 1869 | . 2 ⊢ ∀𝑦(𝜑 → 𝜓) |
4 | 1, 3 | mpg 1871 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1628 ⊆ wss 3721 {copab 4844 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-in 3728 df-ss 3735 df-opab 4845 |
This theorem is referenced by: elopabran 5147 opabssxp 5333 funopab4 6068 ssoprab2i 6895 cnvoprab 7378 cardf2 8968 dfac3 9143 axdc2lem 9471 fpwwe2lem1 9654 canthwe 9674 trclublem 13943 fullfunc 16772 fthfunc 16773 isfull 16776 isfth 16780 ipoval 17361 ipolerval 17363 eqgfval 17849 2ndcctbss 21478 iscgrg 25627 ishpg 25871 pthsfval 26851 spthsfval 26852 crcts 26918 cycls 26919 eupths 27377 nvss 27782 ajfval 27998 afsval 31083 cvmlift2lem12 31628 dicval 36979 areaquad 38321 relopabVD 39653 |
Copyright terms: Public domain | W3C validator |