|   | 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 4066 | . 2 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴} | 
| 3 | abid2 2878 | . 2 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | |
| 4 | 2, 3 | sseqtri 4031 | 1 ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴 | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∈ wcel 2107 {cab 2713 ⊆ wss 3950 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ss 3967 | 
| This theorem is referenced by: ssab2 4078 intab 4977 opabss 5206 relopabiALT 5832 exse2 7940 opiota 8085 mpoexw 8104 fsplitfpar 8144 tfrlem8 8425 fiprc 9086 fival 9453 hartogslem1 9583 dmttrcl 9762 rnttrcl 9763 tz9.12lem1 9828 rankuni 9904 scott0 9927 r0weon 10053 alephval3 10151 aceq3lem 10161 dfac5lem4 10167 dfac5lem4OLD 10169 dfac2b 10172 cff 10289 cfsuc 10298 cff1 10299 cflim2 10304 cfss 10306 axdc3lem 10491 axdclem 10560 gruina 10859 nqpr 11055 infcvgaux1i 15894 4sqlem1 16987 sscpwex 17860 cssval 21701 topnex 23004 islocfin 23526 hauspwpwf1 23996 itg2lcl 25763 2sqlem7 27469 scutf 27858 isismt 28543 nmcexi 32046 opabssi 32626 lsmsnorb 33420 dispcmp 33859 cnre2csqima 33911 mppspstlem 35577 colinearex 36062 itg2addnclem 37679 itg2addnc 37682 eldiophb 42773 | 
| Copyright terms: Public domain | W3C validator |