| 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 4071 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) | |
| 2 | ss2rabi.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
| 3 | 1, 2 | mprgbir 3068 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 {crab 3436 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rab 3437 df-ss 3968 |
| This theorem is referenced by: f1ossf1o 7148 mptexgf 7242 supub 9499 suplub 9500 card2on 9594 rankval4 9907 fin1a2lem12 10451 catlid 17726 catrid 17727 gsumval2 18699 lbsextlem3 21162 psrbagsn 22087 psdmul 22170 musum 27234 ppiub 27248 umgrupgr 29120 umgrislfupgr 29140 usgruspgr 29197 usgrislfuspgr 29204 disjxwwlksn 29924 wwlksnfi 29926 disjxwwlkn 29933 clwwlknclwwlkdifnum 29999 konigsbergssiedgw 30269 omssubadd 34302 bj-unrab 36927 poimirlem26 37653 poimirlem27 37654 ssrabi 38251 lclkrs2 41542 ovolval5lem3 46669 |
| Copyright terms: Public domain | W3C validator |