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 5227. (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 5224 | . . 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 1543 ∈ wcel 2110 {crab 3065 Vcvv 3408 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5192 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-v 3410 df-in 3873 df-ss 3883 |
This theorem is referenced by: rabex2 5227 zorn2lem1 10110 sylow2a 19008 evlslem6 21041 mhpaddcl 21091 mhpvscacl 21094 mretopd 21989 cusgrexilem1 27527 vtxdgf 27559 mntoval 30979 tocycval 31094 prmidlval 31326 evlsbagval 39985 mhpind 39993 stoweidlem35 43251 stoweidlem50 43266 stoweidlem57 43273 stoweidlem59 43275 subsaliuncllem 43571 subsaliuncl 43572 smflimlem1 43978 smflimlem2 43979 smflimlem3 43980 smflimlem6 43983 smfrec 43995 smfpimcclem 44012 smfsuplem1 44016 smfinflem 44022 smflimsuplem1 44025 smflimsuplem2 44026 smflimsuplem3 44027 smflimsuplem4 44028 smflimsuplem5 44029 smflimsuplem7 44031 fvmptrab 44456 prproropen 44633 |
Copyright terms: Public domain | W3C validator |