![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ss2rab | Structured version Visualization version GIF version |
Description: Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.) |
Ref | Expression |
---|---|
ss2rab | ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 3115 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | df-rab 3115 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} | |
3 | 1, 2 | sseq12i 3945 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) |
4 | ss2ab 3987 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓))) | |
5 | df-ral 3111 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓))) | |
6 | imdistan 571 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓))) | |
7 | 6 | albii 1821 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓))) |
8 | 5, 7 | bitr2i 279 | . 2 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
9 | 3, 4, 8 | 3bitri 300 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∀wal 1536 ∈ wcel 2111 {cab 2776 ∀wral 3106 {crab 3110 ⊆ wss 3881 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rab 3115 df-v 3443 df-in 3888 df-ss 3898 |
This theorem is referenced by: ss2rabdv 4003 ss2rabi 4004 mptexgf 6962 scottex 9298 ondomon 9974 eltsms 22738 xrlimcnp 25554 wwlksnfi 27692 disjxwwlkn 27699 occon 29070 spanss 29131 chpssati 30146 lpssat 36309 lssatle 36311 lssat 36312 atlatle 36616 pmaple 37057 diaord 38343 mapdordlem2 38933 rmxyelqirr 39851 itgoss 40107 ovnsslelem 43199 ovolval5lem3 43293 pimiooltgt 43346 preimageiingt 43355 preimaleiinlt 43356 |
Copyright terms: Public domain | W3C validator |