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.) |
Ref | Expression |
---|---|
abssdv.1 | ⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴)) |
Ref | Expression |
---|---|
abssdv | ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abssdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴)) | |
2 | 1 | alrimiv 1930 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 → 𝑥 ∈ 𝐴)) |
3 | abss 3994 | . 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓 → 𝑥 ∈ 𝐴)) | |
4 | 2, 3 | sylibr 233 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1537 ∈ wcel 2106 {cab 2715 ⊆ wss 3887 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-v 3434 df-in 3894 df-ss 3904 |
This theorem is referenced by: dfopifOLD 4801 opabssxpd 5634 fmpt 6984 eroprf 8604 cfslb2n 10024 rankcf 10533 genpv 10755 genpdm 10758 fimaxre3 11921 supadd 11943 supmul 11947 hashfacenOLD 14167 hashf1lem1OLD 14169 hashf1lem2 14170 mertenslem2 15597 4sqlem11 16656 lss1d 20225 lspsn 20264 lpval 22290 lpsscls 22292 ptuni2 22727 ptbasfi 22732 prdstopn 22779 xkopt 22806 tgpconncompeqg 23263 metrest 23680 mbfeqalem1 24805 limcfval 25036 nmosetre 29126 nmopsetretALT 30225 nmfnsetre 30239 sigaclcuni 32086 bnj849 32905 deranglem 33128 derangsn 33132 nosupno 33906 nosupbday 33908 noinfno 33921 noinfbday 33923 liness 34447 mblfinlem3 35816 ismblfin 35818 itg2addnclem 35828 areacirclem2 35866 sdclem2 35900 sdclem1 35901 ismtyval 35958 heibor1lem 35967 heibor1 35968 pmapglbx 37783 eldiophb 40579 hbtlem2 40949 upbdrech 42844 |
Copyright terms: Public domain | W3C validator |