Step |
Hyp |
Ref |
Expression |
1 |
|
fneq2 |
⊢ ( 𝐴 = 𝐵 → ( 𝑓 Fn 𝐴 ↔ 𝑓 Fn 𝐵 ) ) |
2 |
|
raleq |
⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
3 |
1 2
|
anbi12d |
⊢ ( 𝐴 = 𝐵 → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ) |
4 |
3
|
abbidv |
⊢ ( 𝐴 = 𝐵 → { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } = { 𝑓 ∣ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } ) |
5 |
|
dfixp |
⊢ X 𝑥 ∈ 𝐴 𝐶 = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } |
6 |
|
dfixp |
⊢ X 𝑥 ∈ 𝐵 𝐶 = { 𝑓 ∣ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } |
7 |
4 5 6
|
3eqtr4g |
⊢ ( 𝐴 = 𝐵 → X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐵 𝐶 ) |