![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabexd | Structured version Visualization version GIF version |
Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5296. (Contributed by AV, 16-Jul-2019.) |
Ref | Expression |
---|---|
rabexd.1 | ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓} |
rabexd.2 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
Ref | Expression |
---|---|
rabexd | ⊢ (𝜑 → 𝐵 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabexd.1 | . 2 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓} | |
2 | rabexd.2 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
3 | rabexg 5293 | . . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) |
5 | 1, 4 | eqeltrid 2842 | 1 ⊢ (𝜑 → 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 {crab 3410 Vcvv 3448 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-sep 5261 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-in 3922 df-ss 3932 |
This theorem is referenced by: rabex2 5296 zorn2lem1 10439 sylow2a 19408 evlslem6 21507 mhpaddcl 21557 mhpvscacl 21560 mretopd 22459 cusgrexilem1 28429 vtxdgf 28461 mntoval 31884 tocycval 31999 prmidlval 32249 evlsbagval 40777 mhpind 40798 stoweidlem35 44350 stoweidlem50 44365 stoweidlem57 44372 stoweidlem59 44374 subsaliuncllem 44672 subsaliuncl 44673 smflimlem1 45086 smflimlem2 45087 smflimlem3 45088 smflimlem6 45091 smfrec 45104 smfpimcclem 45122 smfsuplem1 45126 smfinflem 45132 smflimsuplem1 45135 smflimsuplem2 45136 smflimsuplem3 45137 smflimsuplem4 45138 smflimsuplem5 45139 smflimsuplem7 45141 fvmptrab 45598 prproropen 45774 |
Copyright terms: Public domain | W3C validator |