| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > abrexex | Structured version Visualization version GIF version | ||
| Description: Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7985. See also abrexex2 7994. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
| Ref | Expression |
|---|---|
| abrexex.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| abrexex | ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abrexex.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | abrexexg 7985 | . 2 ⊢ (𝐴 ∈ V → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 {cab 2714 ∃wrex 3070 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-rep 5279 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-mo 2540 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-v 3482 |
| This theorem is referenced by: ab2rexex 8004 kmlem10 10200 cshwsexa 14862 shftfval 15109 dvdsrval 20361 cmpsublem 23407 cmpsub 23408 ptrescn 23647 addsproplem2 28003 negsid 28073 onaddscl 28286 recut 28428 0reno 28429 satfvsuclem1 35364 fmlasuc0 35389 heibor1lem 37816 pointsetN 39743 eldiophb 42768 |
| Copyright terms: Public domain | W3C validator |