![]() |
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 6660 supub 8653 suplub 8654 card2on 8748 rankval4 9027 fin1a2lem12 9568 catlid 16729 catrid 16730 gsumval2 17666 lbsextlem3 19557 psrbagsn 19891 musum 25369 ppiub 25381 umgrupgr 26451 umgrislfupgr 26471 usgruspgr 26527 usgrislfuspgr 26533 disjxwwlksn 27275 disjxwwlksnOLD 27276 clwwlknclwwlkdifnum 27360 konigsbergssiedgw 27656 omssubadd 30960 bj-unrab 33496 poimirlem26 34061 poimirlem27 34062 ssrabi 34649 lclkrs2 37694 |
Copyright terms: Public domain | W3C validator |