![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ss2rabi | Structured version Visualization version GIF version |
Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.) |
Ref | Expression |
---|---|
ss2rabi.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
ss2rabi | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss2rab 3899 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) | |
2 | ss2rabi.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
3 | 1, 2 | mprgbir 3109 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 {crab 3094 ⊆ wss 3792 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rab 3099 df-in 3799 df-ss 3806 |
This theorem is referenced by: f1ossf1o 6662 supub 8655 suplub 8656 card2on 8750 rankval4 9029 fin1a2lem12 9570 catlid 16733 catrid 16734 gsumval2 17670 lbsextlem3 19561 psrbagsn 19895 musum 25373 ppiub 25385 umgrupgr 26455 umgrislfupgr 26475 usgruspgr 26531 usgrislfuspgr 26537 disjxwwlksn 27279 disjxwwlksnOLD 27280 clwwlknclwwlkdifnum 27364 konigsbergssiedgw 27660 omssubadd 30964 bj-unrab 33500 poimirlem26 34066 poimirlem27 34067 ssrabi 34654 lclkrs2 37699 |
Copyright terms: Public domain | W3C validator |