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 5424 | . 2 ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) | |
2 | ssopab2i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 2 | ax-gen 1787 | . 2 ⊢ ∀𝑦(𝜑 → 𝜓) |
4 | 1, 3 | mpg 1789 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 ⊆ wss 3933 {copab 5119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-in 3940 df-ss 3949 df-opab 5120 |
This theorem is referenced by: elopabran 5439 opabssxp 5636 relopabiv 5686 funopab4 6385 ssoprab2i 7252 cnvoprab 7747 cardf2 9360 dfac3 9535 axdc2lem 9858 fpwwe2lem1 10041 canthwe 10061 trclublem 14343 fullfunc 17164 fthfunc 17165 isfull 17168 isfth 17172 ipoval 17752 ipolerval 17754 eqgfval 18266 2ndcctbss 21991 iscgrg 26225 ishpg 26472 pthsfval 27429 spthsfval 27430 crcts 27496 cycls 27497 eupths 27906 nvss 28297 ajfval 28513 afsval 31841 cvmlift2lem12 32458 satf0suclem 32519 fmlasuc0 32528 bj-opabssvv 34334 bj-imdirval2 34365 dicval 38192 areaquad 39701 relopabVD 41112 |
Copyright terms: Public domain | W3C validator |