| 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 3062 | . 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒)) | |
| 2 | df-clab 2715 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | |
| 3 | ralab.1 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | sbievw 2093 | . . . . . 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 1819 | . 2 ⊢ (∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ ∀𝑥(𝜓 → 𝜒)) |
| 10 | 1, 9 | bitri 275 | 1 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 [wsb 2064 ∈ wcel 2108 {cab 2714 ∀wral 3061 |
| 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-ral 3062 |
| This theorem is referenced by: rexab 3700 ralrnmpo 7572 funcnvuni 7954 kardex 9934 karden 9935 fimaxre3 12214 ptcnp 23630 ptrescn 23647 itg2leub 25769 addsuniflem 28034 addsbdaylem 28049 mulsuniflem 28175 nmoubi 30791 nmopub 31927 nmfnleub 31944 nmcexi 32045 mblfinlem3 37666 ismblfin 37668 itg2addnc 37681 hbtlem2 43136 oaun3lem1 43387 |
| Copyright terms: Public domain | W3C validator |