| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ss2abi | Structured version Visualization version GIF version | ||
| Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2110, ax-10 2141, ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.) |
| Ref | Expression |
|---|---|
| ss2abi.1 | ⊢ (𝜑 → 𝜓) |
| Ref | Expression |
|---|---|
| ss2abi | ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tru 1544 | . 2 ⊢ ⊤ | |
| 2 | ss2abi.1 | . . . 4 ⊢ (𝜑 → 𝜓) | |
| 3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → (𝜑 → 𝜓)) |
| 4 | 3 | ss2abdv 4066 | . 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}) |
| 5 | 1, 4 | ax-mp 5 | 1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊤wtru 1541 {cab 2714 ⊆ wss 3951 |
| 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 |
| This theorem depends on definitions: df-bi 207 df-tru 1543 df-sb 2065 df-clab 2715 df-ss 3968 |
| This theorem is referenced by: abssi 4070 rabssab 4085 abanssl 4311 abanssr 4312 pwpwssunieq 5104 intabs 5349 abssexg 5382 imassrn 6089 fvclss 7261 fabexgOLD 7961 mapex 7963 f1oabexgOLD 7965 mapexOLD 8872 f1osetex 8899 fsetexb 8904 tc2 9782 hta 9937 infmap2 10257 cflm 10290 cflim2 10303 hsmex3 10474 domtriomlem 10482 axdc3lem2 10491 brdom7disj 10571 brdom6disj 10572 npex 11026 hashf1lem2 14495 issubc 17880 isghmOLD 19234 symgbas 19389 symgbasfi 19396 tgval 22962 ustfn 24210 ustval 24211 ustn0 24229 birthdaylem1 26994 nosupno 27748 rgrprc 29609 wksfval 29627 mptctf 32729 measbase 34198 measval 34199 ismeas 34200 isrnmeas 34201 ballotlem2 34491 subfaclefac 35181 satfvsuclem1 35364 dfon2lem2 35785 poimirlem4 37631 poimirlem9 37636 poimirlem26 37653 poimirlem27 37654 poimirlem28 37655 poimirlem32 37659 sdclem2 37749 lineset 39740 lautset 40084 pautsetN 40100 tendoset 40761 eldiophb 42768 rmxyelqirr 42921 hbtlem1 43135 hbtlem7 43137 relopabVD 44921 rabexgf 45029 prprval 47501 upwlksfval 48051 |
| Copyright terms: Public domain | W3C validator |