![]() |
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 3060 | . 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒)) | |
2 | df-clab 2713 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | |
3 | ralab.1 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
4 | 3 | sbievw 2091 | . . . . . 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 1816 | . 2 ⊢ (∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ ∀𝑥(𝜓 → 𝜒)) |
10 | 1, 9 | bitri 275 | 1 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 [wsb 2062 ∈ wcel 2106 {cab 2712 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-ral 3060 |
This theorem is referenced by: rexab 3703 ralrnmpo 7572 funcnvuni 7955 kardex 9932 karden 9933 fimaxre3 12212 ptcnp 23646 ptrescn 23663 itg2leub 25784 addsuniflem 28049 addsbdaylem 28064 mulsuniflem 28190 nmoubi 30801 nmopub 31937 nmfnleub 31954 nmcexi 32055 mblfinlem3 37646 ismblfin 37648 itg2addnc 37661 hbtlem2 43113 oaun3lem1 43364 |
Copyright terms: Public domain | W3C validator |