![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > abssi | Structured version Visualization version GIF version |
Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) |
Ref | Expression |
---|---|
abssi.1 | ⊢ (𝜑 → 𝑥 ∈ 𝐴) |
Ref | Expression |
---|---|
abssi | ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abssi.1 | . . 3 ⊢ (𝜑 → 𝑥 ∈ 𝐴) | |
2 | 1 | ss2abi 4063 | . 2 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴} |
3 | abid2 2872 | . 2 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | |
4 | 2, 3 | sseqtri 4018 | 1 ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 {cab 2710 ⊆ wss 3948 |
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-8 2109 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-clel 2811 df-v 3477 df-in 3955 df-ss 3965 |
This theorem is referenced by: ssab2 4076 intab 4982 opabss 5212 relopabiALT 5822 exse2 7905 opiota 8042 mpoexw 8062 fsplitfpar 8101 tfrlem8 8381 fiprc 9042 fival 9404 hartogslem1 9534 dmttrcl 9713 rnttrcl 9714 tz9.12lem1 9779 rankuni 9855 scott0 9878 r0weon 10004 alephval3 10102 aceq3lem 10112 dfac5lem4 10118 dfac2b 10122 cff 10240 cfsuc 10249 cff1 10250 cflim2 10255 cfss 10257 axdc3lem 10442 axdclem 10511 gruina 10810 nqpr 11006 infcvgaux1i 15800 4sqlem1 16878 sscpwex 17759 cssval 21227 topnex 22491 islocfin 23013 hauspwpwf1 23483 itg2lcl 25237 2sqlem7 26917 scutf 27303 isismt 27775 nmcexi 31267 opabssi 31830 lsmsnorb 32490 dispcmp 32828 cnre2csqima 32880 mppspstlem 34551 colinearex 35021 itg2addnclem 36528 itg2addnc 36531 eldiophb 41481 |
Copyright terms: Public domain | W3C validator |