| 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 5341. (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 5337 | . . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) | |
| 4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) |
| 5 | 1, 4 | eqeltrid 2845 | 1 ⊢ (𝜑 → 𝐵 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 {crab 3436 Vcvv 3480 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: rabex2 5341 zorn2lem1 10536 sylow2a 19637 psrascl 21999 evlslem6 22105 mhpaddcl 22155 mhmcompl 22384 mhmcoaddmpl 22385 mretopd 23100 cusgrexilem1 29456 vtxdgf 29489 mntoval 32972 tocycval 33128 prmidlval 33465 isprimroot 42094 primrootsunit1 42098 unitscyglem1 42196 evlsvvval 42573 evlsbagval 42576 mhpind 42604 stoweidlem35 46050 stoweidlem50 46065 stoweidlem57 46072 stoweidlem59 46074 subsaliuncllem 46372 subsaliuncl 46373 smflimlem1 46786 smflimlem2 46787 smflimlem3 46788 smflimlem6 46791 smfrec 46804 smfpimcclem 46822 smfsuplem1 46826 smfinflem 46832 smflimsuplem1 46835 smflimsuplem2 46836 smflimsuplem3 46837 smflimsuplem4 46838 smflimsuplem5 46839 smflimsuplem7 46841 fvmptrab 47304 prproropen 47495 stgrvtx 47921 stgriedg 47922 gpgvtx 48002 gpgiedg 48003 |
| Copyright terms: Public domain | W3C validator |