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 1919 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 → 𝑥 ∈ 𝐴)) |
3 | abss 4037 | . 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓 → 𝑥 ∈ 𝐴)) | |
4 | 2, 3 | sylibr 235 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 ∈ wcel 2105 {cab 2796 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-in 3940 df-ss 3949 |
This theorem is referenced by: dfopif 4792 opabssxpd 5782 fmpt 6866 eroprf 8384 cfslb2n 9678 rankcf 10187 genpv 10409 genpdm 10412 fimaxre3 11575 supadd 11597 supmul 11601 hashfacen 13800 hashf1lem1 13801 hashf1lem2 13802 mertenslem2 15229 4sqlem11 16279 symgbas 18436 lss1d 19664 lspsn 19703 lpval 21675 lpsscls 21677 ptuni2 22112 ptbasfi 22117 prdstopn 22164 xkopt 22191 tgpconncompeqg 22647 metrest 23061 mbfeqalem1 24169 limcfval 24397 nmosetre 28468 nmopsetretALT 29567 nmfnsetre 29581 sigaclcuni 31276 bnj849 32096 deranglem 32310 derangsn 32314 nosupno 33100 nosupbday 33102 liness 33503 mblfinlem3 34812 ismblfin 34814 itg2addnclem 34824 areacirclem2 34864 sdclem2 34898 sdclem1 34899 ismtyval 34959 heibor1lem 34968 heibor1 34969 pmapglbx 36785 eldiophb 39232 hbtlem2 39602 upbdrech 41448 |
Copyright terms: Public domain | W3C validator |