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 5228. (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 5225 | . . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) |
5 | 1, 4 | eqeltrid 2915 | 1 ⊢ (𝜑 → 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1531 ∈ wcel 2108 {crab 3140 Vcvv 3493 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-rab 3145 df-v 3495 df-in 3941 df-ss 3950 |
This theorem is referenced by: rabex2 5228 zorn2lem1 9910 sylow2a 18736 evlslem6 20286 mhpaddcl 20330 mhpinvcl 20331 mhpvscacl 20333 mretopd 21692 cusgrexilem1 27213 vtxdgf 27245 tocycval 30743 prmidlval 30947 stoweidlem35 42311 stoweidlem50 42326 stoweidlem57 42333 stoweidlem59 42335 subsaliuncllem 42631 subsaliuncl 42632 smflimlem1 43038 smflimlem2 43039 smflimlem3 43040 smflimlem6 43043 smfrec 43055 smfpimcclem 43072 smfsuplem1 43076 smfinflem 43082 smflimsuplem1 43085 smflimsuplem2 43086 smflimsuplem3 43087 smflimsuplem4 43088 smflimsuplem5 43089 smflimsuplem7 43091 fvmptrab 43482 prproropen 43661 |
Copyright terms: Public domain | W3C validator |