![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexrab | Structured version Visualization version GIF version |
Description: Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.) |
Ref | Expression |
---|---|
ralab.1 | ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexrab | ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralab.1 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
2 | 1 | elrab 3684 | . . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | anbi1i 625 | . . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∧ 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) ∧ 𝜒)) |
4 | anass 470 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) ∧ 𝜒) ↔ (𝑥 ∈ 𝐴 ∧ (𝜓 ∧ 𝜒))) | |
5 | 3, 4 | bitri 275 | . 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∧ 𝜒) ↔ (𝑥 ∈ 𝐴 ∧ (𝜓 ∧ 𝜒))) |
6 | 5 | rexbii2 3091 | 1 ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∈ wcel 2107 ∃wrex 3071 {crab 3433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rex 3072 df-rab 3434 df-v 3477 |
This theorem is referenced by: wereu2 5674 frpomin 6342 wdom2d 9575 enfin2i 10316 infm3 12173 pmtrfrn 19326 pgpssslw 19482 ellspd 21357 1stcfb 22949 xkobval 23090 xkococn 23164 imasdsf1olem 23879 eqscut2 27307 scutun12 27311 cuteq0 27333 rusgrnumwwlks 29228 cvmliftlem15 34289 wsuclem 34797 poimirlem4 36492 poimirlem26 36514 poimirlem27 36515 infdesc 41385 rexrabdioph 41532 hbtlem6 41871 |
Copyright terms: Public domain | W3C validator |