![]() |
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 5289. (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 5286 | . . 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 1541 ∈ wcel 2106 {crab 3405 Vcvv 3443 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5254 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3406 df-v 3445 df-in 3915 df-ss 3925 |
This theorem is referenced by: rabex2 5289 zorn2lem1 10428 sylow2a 19392 evlslem6 21475 mhpaddcl 21525 mhpvscacl 21528 mretopd 22427 cusgrexilem1 28273 vtxdgf 28305 mntoval 31725 tocycval 31840 prmidlval 32088 evlsbagval 40699 mhpind 40707 stoweidlem35 44208 stoweidlem50 44223 stoweidlem57 44230 stoweidlem59 44232 subsaliuncllem 44530 subsaliuncl 44531 smflimlem1 44944 smflimlem2 44945 smflimlem3 44946 smflimlem6 44949 smfrec 44962 smfpimcclem 44980 smfsuplem1 44984 smfinflem 44990 smflimsuplem1 44993 smflimsuplem2 44994 smflimsuplem3 44995 smflimsuplem4 44996 smflimsuplem5 44997 smflimsuplem7 44999 fvmptrab 45456 prproropen 45632 |
Copyright terms: Public domain | W3C validator |