![]() |
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 4021 | . 2 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴}) |
3 | abid1 2871 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | |
4 | 2, 3 | sseqtrrdi 3996 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 {cab 2710 ⊆ wss 3911 |
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 3446 df-in 3918 df-ss 3928 |
This theorem is referenced by: dfopif 4828 opabssxpd 5680 fmpt 7059 eroprf 8757 cfslb2n 10209 rankcf 10718 genpv 10940 genpdm 10943 fimaxre3 12106 supadd 12128 supmul 12132 hashfacenOLD 14358 hashf1lem1OLD 14360 hashf1lem2 14361 mertenslem2 15775 4sqlem11 16832 lss1d 20439 lspsn 20478 lpval 22506 lpsscls 22508 ptuni2 22943 ptbasfi 22948 prdstopn 22995 xkopt 23022 tgpconncompeqg 23479 metrest 23896 mbfeqalem1 25021 limcfval 25252 nosupno 27067 nosupbday 27069 noinfno 27082 noinfbday 27084 addsproplem2 27304 addsunif 27332 negsid 27361 mulsproplem10 27410 nmosetre 29748 nmopsetretALT 30847 nmfnsetre 30861 sigaclcuni 32774 bnj849 33594 deranglem 33817 derangsn 33821 liness 34776 mblfinlem3 36163 ismblfin 36165 itg2addnclem 36175 areacirclem2 36213 sdclem2 36247 sdclem1 36248 ismtyval 36305 heibor1lem 36314 heibor1 36315 pmapglbx 38278 eldiophb 41123 hbtlem2 41494 oaun3lem1 41733 oaun3lem2 41734 upbdrech 43626 |
Copyright terms: Public domain | W3C validator |