![]() |
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 2101, ax-10 2130, ax-11 2147, ax-12 2167. (Revised by GG, 28-Jun-2024.) |
Ref | Expression |
---|---|
ss2abi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ss2abi | ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1538 | . 2 ⊢ ⊤ | |
2 | ss2abi.1 | . . . 4 ⊢ (𝜑 → 𝜓) | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → (𝜑 → 𝜓)) |
4 | 3 | ss2abdv 4060 | . 2 ⊢ (⊤ → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊤wtru 1535 {cab 2703 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-tru 1537 df-sb 2061 df-clab 2704 df-ss 3964 |
This theorem is referenced by: abssi 4066 rabssab 4082 abanssl 4303 abanssr 4304 pwpwssunieq 5112 intabs 5349 abssexg 5386 imassrn 6080 fvclss 7256 fabexgOLD 7950 mapex 7952 f1oabexgOLD 7954 mapexOLD 8861 f1osetex 8888 fsetexb 8893 tc2 9785 hta 9940 infmap2 10261 cflm 10293 cflim2 10306 hsmex3 10477 domtriomlem 10485 axdc3lem2 10494 brdom7disj 10574 brdom6disj 10575 npex 11029 hashf1lem2 14475 issubc 17854 isghmOLD 19210 permsetexOLD 19367 symgbas 19368 symgbasfi 19376 tgval 22949 ustfn 24197 ustval 24198 ustn0 24216 birthdaylem1 26979 nosupno 27733 rgrprc 29528 wksfval 29546 mptctf 32631 measbase 34030 measval 34031 ismeas 34032 isrnmeas 34033 ballotlem2 34322 subfaclefac 35004 satfvsuclem1 35187 dfon2lem2 35608 poimirlem4 37325 poimirlem9 37330 poimirlem26 37347 poimirlem27 37348 poimirlem28 37349 poimirlem32 37353 sdclem2 37443 lineset 39437 lautset 39781 pautsetN 39797 tendoset 40458 eldiophb 42414 rmxyelqirr 42567 hbtlem1 42784 hbtlem7 42786 relopabVD 44577 rabexgf 44623 prprval 47086 upwlksfval 47512 |
Copyright terms: Public domain | W3C validator |