![]() |
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 4081 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) | |
2 | ss2rabi.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
3 | 1, 2 | mprgbir 3066 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 {crab 3433 ⊆ wss 3963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ral 3060 df-rab 3434 df-ss 3980 |
This theorem is referenced by: f1ossf1o 7148 mptexgf 7242 supub 9497 suplub 9498 card2on 9592 rankval4 9905 fin1a2lem12 10449 catlid 17728 catrid 17729 gsumval2 18712 lbsextlem3 21180 psrbagsn 22105 psdmul 22188 musum 27249 ppiub 27263 umgrupgr 29135 umgrislfupgr 29155 usgruspgr 29212 usgrislfuspgr 29219 disjxwwlksn 29934 wwlksnfi 29936 disjxwwlkn 29943 clwwlknclwwlkdifnum 30009 konigsbergssiedgw 30279 omssubadd 34282 bj-unrab 36909 poimirlem26 37633 poimirlem27 37634 ssrabi 38232 lclkrs2 41523 ovolval5lem3 46610 |
Copyright terms: Public domain | W3C validator |