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 3602 | . . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | anbi1i 627 | . . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∧ 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) ∧ 𝜒)) |
4 | anass 472 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) ∧ 𝜒) ↔ (𝑥 ∈ 𝐴 ∧ (𝜓 ∧ 𝜒))) | |
5 | 3, 4 | bitri 278 | . 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∧ 𝜒) ↔ (𝑥 ∈ 𝐴 ∧ (𝜓 ∧ 𝜒))) |
6 | 5 | rexbii2 3168 | 1 ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2110 ∃wrex 3062 {crab 3065 |
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 |
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-rex 3067 df-rab 3070 df-v 3410 |
This theorem is referenced by: wereu2 5548 frpomin 6194 wdom2d 9196 enfin2i 9935 infm3 11791 pmtrfrn 18850 pgpssslw 19003 ellspd 20764 1stcfb 22342 xkobval 22483 xkococn 22557 imasdsf1olem 23271 rusgrnumwwlks 28058 cvmliftlem15 32973 wsuclem 33556 eqscut2 33737 scutun12 33741 poimirlem4 35518 poimirlem26 35540 poimirlem27 35541 infdesc 40183 rexrabdioph 40319 hbtlem6 40657 |
Copyright terms: Public domain | W3C validator |