| 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 5551 | . 2 ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) | |
| 2 | ssopab2i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 3 | 2 | ax-gen 1795 | . 2 ⊢ ∀𝑦(𝜑 → 𝜓) |
| 4 | 1, 3 | mpg 1797 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ⊆ wss 3951 {copab 5205 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-ss 3968 df-opab 5206 |
| This theorem is referenced by: elopabran 5567 elopaelxp 5775 opabssxp 5778 relopabiv 5830 funopab4 6603 ssoprab2i 7544 cnvoprab 8085 mptmpoopabbrd 8105 cardf2 9983 dfac3 10161 axdc2lem 10488 fpwwe2lem1 10671 canthwe 10691 trclublem 15034 fullfunc 17953 fthfunc 17954 isfull 17957 isfth 17961 ipoval 18575 ipolerval 18577 eqgfval 19194 2ndcctbss 23463 iscgrg 28520 ishpg 28767 nvss 30612 ajfval 30828 afsval 34686 cvmlift2lem12 35319 satf0suclem 35380 fmlasuc0 35389 bj-opabssvv 37151 bj-imdirval2lem 37183 bj-xpcossxp 37190 dicval 41178 areaquad 43228 relopabVD 44921 |
| Copyright terms: Public domain | W3C validator |