| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ralab | Structured version Visualization version GIF version | ||
| Description: Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) Reduce axiom usage. (Revised by GG, 2-Nov-2024.) |
| Ref | Expression |
|---|---|
| ralab.1 | ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| ralab | ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ral 3052 | . 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒)) | |
| 2 | df-clab 2715 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | |
| 3 | ralab.1 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | sbievw 2098 | . . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 ↔ 𝜓) |
| 5 | 2, 4 | bitri 275 | . . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ 𝜓) |
| 6 | 5 | imbi1i 349 | . . . 4 ⊢ ((𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ (𝜓 → 𝜒)) |
| 7 | biid 261 | . . . 4 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜒)) | |
| 8 | 6, 7 | bitri 275 | . . 3 ⊢ ((𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ (𝜓 → 𝜒)) |
| 9 | 8 | albii 1820 | . 2 ⊢ (∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ ∀𝑥(𝜓 → 𝜒)) |
| 10 | 1, 9 | bitri 275 | 1 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1539 [wsb 2067 ∈ wcel 2113 {cab 2714 ∀wral 3051 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-sb 2068 df-clab 2715 df-ral 3052 |
| This theorem is referenced by: rexab 3653 ralrnmpo 7497 funcnvuni 7874 kardex 9806 karden 9807 fimaxre3 12088 ptcnp 23566 ptrescn 23583 itg2leub 25691 addsuniflem 27997 addbdaylem 28013 mulsuniflem 28145 nmoubi 30847 nmopub 31983 nmfnleub 32000 nmcexi 32101 mblfinlem3 37860 ismblfin 37862 itg2addnc 37875 hbtlem2 43366 oaun3lem1 43616 |
| Copyright terms: Public domain | W3C validator |