![]() |
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.) |
Ref | Expression |
---|---|
ss2abi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ss2abi | ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss2ab 3891 | . 2 ⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓)) | |
2 | ss2abi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpgbir 1843 | 1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 {cab 2763 ⊆ wss 3792 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-in 3799 df-ss 3806 |
This theorem is referenced by: abssi 3898 rabssab 3912 pwpwssunieq 4849 intabs 5059 abssexg 5093 imassrn 5731 fvclss 6772 fabexg 7401 f1oabexg 7404 mapex 8146 tc2 8915 hta 9057 infmap2 9375 cflm 9407 cflim2 9420 hsmex3 9591 domtriomlem 9599 axdc3lem2 9608 brdom7disj 9688 brdom6disj 9689 npex 10143 hashf1lem2 13554 issubc 16880 isghm 18044 symgbasfi 18189 tgval 21167 ustfn 22413 ustval 22414 ustn0 22432 birthdaylem1 25130 rgrprc 26939 wksfval 26957 mptctf 30061 measbase 30858 measval 30859 ismeas 30860 isrnmeas 30861 ballotlem2 31149 subfaclefac 31757 dfon2lem2 32277 nosupno 32438 cnfinltrel 33836 poimirlem4 34041 poimirlem9 34046 poimirlem26 34063 poimirlem27 34064 poimirlem28 34065 poimirlem32 34069 sdclem2 34164 lineset 35894 lautset 36238 pautsetN 36254 tendoset 36915 eldiophb 38284 hbtlem1 38656 hbtlem7 38658 relopabVD 40074 rabexgf 40120 prprval 42457 upwlksfval 42762 |
Copyright terms: Public domain | W3C validator |