| 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 3046 | . 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒)) | |
| 2 | df-clab 2709 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | |
| 3 | ralab.1 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | sbievw 2095 | . . . . . 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 2066 ∈ wcel 2110 {cab 2708 ∀wral 3045 |
| 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 2067 df-clab 2709 df-ral 3046 |
| This theorem is referenced by: rexab 3652 ralrnmpo 7480 funcnvuni 7857 kardex 9779 karden 9780 fimaxre3 12060 ptcnp 23530 ptrescn 23547 itg2leub 25655 addsuniflem 27937 addsbdaylem 27952 mulsuniflem 28081 nmoubi 30742 nmopub 31878 nmfnleub 31895 nmcexi 31996 mblfinlem3 37678 ismblfin 37680 itg2addnc 37693 hbtlem2 43136 oaun3lem1 43386 |
| Copyright terms: Public domain | W3C validator |