| 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 3692 | . . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
| 3 | 2 | anbi1i 624 | . . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∧ 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) ∧ 𝜒)) |
| 4 | anass 468 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) ∧ 𝜒) ↔ (𝑥 ∈ 𝐴 ∧ (𝜓 ∧ 𝜒))) | |
| 5 | 3, 4 | bitri 275 | . 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∧ 𝜒) ↔ (𝑥 ∈ 𝐴 ∧ (𝜓 ∧ 𝜒))) |
| 6 | 5 | rexbii2 3090 | 1 ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2108 ∃wrex 3070 {crab 3436 |
| 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-rab 3437 df-v 3482 |
| This theorem is referenced by: wereu2 5682 frpomin 6361 wdom2d 9620 enfin2i 10361 infm3 12227 pmtrfrn 19476 pgpssslw 19632 ellspd 21822 1stcfb 23453 xkobval 23594 xkococn 23668 imasdsf1olem 24383 eqscut2 27851 scutun12 27855 cuteq0 27877 rusgrnumwwlks 29994 cvmliftlem15 35303 wsuclem 35826 poimirlem4 37631 poimirlem26 37653 poimirlem27 37654 infdesc 42653 rexrabdioph 42805 hbtlem6 43141 uhgrimisgrgric 47899 uspgrlimlem1 47955 |
| Copyright terms: Public domain | W3C validator |