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 4049 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) | |
2 | ss2rabi.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
3 | 1, 2 | mprgbir 3155 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 {crab 3144 ⊆ wss 3938 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rab 3149 df-in 3945 df-ss 3954 |
This theorem is referenced by: f1ossf1o 6892 supub 8925 suplub 8926 card2on 9020 rankval4 9298 fin1a2lem12 9835 catlid 16956 catrid 16957 gsumval2 17898 lbsextlem3 19934 psrbagsn 20277 musum 25770 ppiub 25782 umgrupgr 26890 umgrislfupgr 26910 usgruspgr 26965 usgrislfuspgr 26971 disjxwwlksn 27684 clwwlknclwwlkdifnum 27760 konigsbergssiedgw 28031 omssubadd 31560 bj-unrab 34246 poimirlem26 34920 poimirlem27 34921 ssrabi 35513 lclkrs2 38678 |
Copyright terms: Public domain | W3C validator |