![]() |
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 2109, ax-10 2138, ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.) |
Ref | Expression |
---|---|
ss2abi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ss2abi | ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1546 | . 2 ⊢ ⊤ | |
2 | ss2abi.1 | . . . 4 ⊢ (𝜑 → 𝜓) | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → (𝜑 → 𝜓)) |
4 | 3 | ss2abdv 4021 | . 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊤wtru 1543 {cab 2710 ⊆ wss 3911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-in 3918 df-ss 3928 |
This theorem is referenced by: abssi 4028 rabssab 4044 abanssl 4262 abanssr 4263 pwpwssunieq 5065 intabs 5300 abssexg 5338 imassrn 6025 fvclss 7190 fabexg 7872 f1oabexg 7874 mapex 8774 f1osetex 8800 fsetexb 8805 tc2 9683 hta 9838 infmap2 10159 cflm 10191 cflim2 10204 hsmex3 10375 domtriomlem 10383 axdc3lem2 10392 brdom7disj 10472 brdom6disj 10473 npex 10927 hashf1lem2 14361 issubc 17726 isghm 19013 permsetexOLD 19156 symgbas 19157 symgbasfi 19165 tgval 22321 ustfn 23569 ustval 23570 ustn0 23588 birthdaylem1 26317 nosupno 27067 rgrprc 28581 wksfval 28599 mptctf 31681 measbase 32853 measval 32854 ismeas 32855 isrnmeas 32856 ballotlem2 33145 subfaclefac 33827 satfvsuclem1 34010 dfon2lem2 34415 poimirlem4 36128 poimirlem9 36133 poimirlem26 36150 poimirlem27 36151 poimirlem28 36152 poimirlem32 36156 sdclem2 36247 lineset 38247 lautset 38591 pautsetN 38607 tendoset 39268 eldiophb 41123 rmxyelqirr 41276 hbtlem1 41493 hbtlem7 41495 relopabVD 43271 rabexgf 43317 prprval 45792 upwlksfval 46123 |
Copyright terms: Public domain | W3C validator |