Step |
Hyp |
Ref |
Expression |
1 |
|
cbvraldva2.1 |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) |
2 |
|
cbvraldva2.2 |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) |
3 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 ) |
4 |
3 2
|
eleq12d |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) ) |
5 |
4 1
|
imbi12d |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) |
6 |
5
|
expcom |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) ) |
7 |
6
|
pm5.74d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜓 ) ) ↔ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) ) |
8 |
7
|
cbvalvw |
⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜓 ) ) ↔ ∀ 𝑦 ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) |
9 |
|
19.21v |
⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ) ) |
10 |
|
19.21v |
⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ↔ ( 𝜑 → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) |
11 |
8 9 10
|
3bitr3i |
⊢ ( ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) |
12 |
11
|
pm5.74ri |
⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) |
13 |
|
df-ral |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ) |
14 |
|
df-ral |
⊢ ( ∀ 𝑦 ∈ 𝐵 𝜒 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜒 ) ) |
15 |
12 13 14
|
3bitr4g |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑦 ∈ 𝐵 𝜒 ) ) |