![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralxfr2d | Structured version Visualization version GIF version |
Description: Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) |
Ref | Expression |
---|---|
ralxfr2d.1 | ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) |
ralxfr2d.2 | ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) |
ralxfr2d.3 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralxfr2d | ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralxfr2d.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) | |
2 | elisset 3452 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | syl 17 | . . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃𝑥 𝑥 = 𝐴) |
4 | ralxfr2d.2 | . . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) | |
5 | 4 | biimprd 251 | . . . . . . 7 ⊢ (𝜑 → (∃𝑦 ∈ 𝐶 𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
6 | r19.23v 3238 | . . . . . . 7 ⊢ (∀𝑦 ∈ 𝐶 (𝑥 = 𝐴 → 𝑥 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐶 𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) | |
7 | 5, 6 | sylibr 237 | . . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐶 (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
8 | 7 | r19.21bi 3173 | . . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
9 | eleq1 2877 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
10 | 8, 9 | mpbidi 244 | . . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 → 𝐴 ∈ 𝐵)) |
11 | 10 | exlimdv 1934 | . . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵)) |
12 | 3, 11 | mpd 15 | . 2 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) |
13 | 4 | biimpa 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) |
14 | ralxfr2d.3 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) | |
15 | 12, 13, 14 | ralxfrd 5274 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∃wex 1781 ∈ wcel 2111 ∀wral 3106 ∃wrex 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-cleq 2791 df-clel 2870 df-ral 3111 df-rex 3112 |
This theorem is referenced by: rexxfr2d 5277 ralrn 6831 ralima 6978 cnrest2 21891 cnprest2 21895 connsuba 22025 subislly 22086 trfbas2 22448 trfil2 22492 flimrest 22588 fclsrest 22629 tsmssubm 22748 metucn 23178 ist0cld 31186 extoimad 40868 |
Copyright terms: Public domain | W3C validator |