| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > abssdv | Structured version Visualization version GIF version | ||
| Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) (Proof shortened by SN, 22-Dec-2024.) |
| Ref | Expression |
|---|---|
| abssdv.1 | ⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴)) |
| Ref | Expression |
|---|---|
| abssdv | ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abssdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴)) | |
| 2 | 1 | ss2abdv 4066 | . 2 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴}) |
| 3 | abid1 2878 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | |
| 4 | 2, 3 | sseqtrrdi 4025 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 {cab 2714 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 |
| This theorem is referenced by: dfopif 4870 opabssxpd 5732 fmpt 7130 fabexd 7959 eroprf 8855 cfslb2n 10308 rankcf 10817 genpv 11039 genpdm 11042 fimaxre3 12214 supadd 12236 supmul 12240 hashf1lem2 14495 mertenslem2 15921 4sqlem11 16993 lss1d 20961 lspsn 21000 lpval 23147 lpsscls 23149 ptuni2 23584 ptbasfi 23589 prdstopn 23636 xkopt 23663 tgpconncompeqg 24120 metrest 24537 mbfeqalem1 25676 limcfval 25907 nosupno 27748 nosupbday 27750 noinfno 27763 noinfbday 27765 addsproplem2 28003 addsuniflem 28034 addsbdaylem 28049 negsid 28073 mulsproplem9 28150 ssltmul1 28173 ssltmul2 28174 precsexlem8 28238 precsexlem11 28241 onaddscl 28286 onmulscl 28287 recut 28428 0reno 28429 nmosetre 30783 nmopsetretALT 31882 nmfnsetre 31896 sigaclcuni 34119 bnj849 34939 deranglem 35171 derangsn 35175 liness 36146 mblfinlem3 37666 ismblfin 37668 itg2addnclem 37678 areacirclem2 37716 sdclem2 37749 sdclem1 37750 ismtyval 37807 heibor1lem 37816 heibor1 37817 pmapglbx 39771 eldiophb 42768 hbtlem2 43136 oaun3lem1 43387 oaun3lem2 43388 upbdrech 45317 |
| Copyright terms: Public domain | W3C validator |