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 1934 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 → 𝑥 ∈ 𝐴)) |
3 | abss 3950 | . 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓 → 𝑥 ∈ 𝐴)) | |
4 | 2, 3 | sylibr 237 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ∈ wcel 2114 {cab 2716 ⊆ wss 3843 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-v 3400 df-in 3850 df-ss 3860 |
This theorem is referenced by: dfopifOLD 4756 opabssxpd 5570 fmpt 6884 eroprf 8426 cfslb2n 9768 rankcf 10277 genpv 10499 genpdm 10502 fimaxre3 11664 supadd 11686 supmul 11690 hashfacenOLD 13905 hashf1lem1OLD 13907 hashf1lem2 13908 mertenslem2 15333 4sqlem11 16391 lss1d 19854 lspsn 19893 lpval 21890 lpsscls 21892 ptuni2 22327 ptbasfi 22332 prdstopn 22379 xkopt 22406 tgpconncompeqg 22863 metrest 23277 mbfeqalem1 24393 limcfval 24624 nmosetre 28699 nmopsetretALT 29798 nmfnsetre 29812 sigaclcuni 31656 bnj849 32476 deranglem 32699 derangsn 32703 nosupno 33547 nosupbday 33549 noinfno 33562 noinfbday 33564 liness 34085 mblfinlem3 35439 ismblfin 35441 itg2addnclem 35451 areacirclem2 35489 sdclem2 35523 sdclem1 35524 ismtyval 35581 heibor1lem 35590 heibor1 35591 pmapglbx 37406 eldiophb 40151 hbtlem2 40521 upbdrech 42382 |
Copyright terms: Public domain | W3C validator |