Step |
Hyp |
Ref |
Expression |
1 |
|
an4 |
⊢ ( ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( ( 𝑓 Fn 𝐴 ∧ 𝑓 Fn 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ) |
2 |
|
anidm |
⊢ ( ( 𝑓 Fn 𝐴 ∧ 𝑓 Fn 𝐴 ) ↔ 𝑓 Fn 𝐴 ) |
3 |
|
r19.26 |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
4 |
|
elin |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
5 |
4
|
bicomi |
⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) |
6 |
5
|
ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) |
7 |
3 6
|
bitr3i |
⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) |
8 |
2 7
|
anbi12i |
⊢ ( ( ( 𝑓 Fn 𝐴 ∧ 𝑓 Fn 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) ) |
9 |
1 8
|
bitri |
⊢ ( ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) ) |
10 |
|
vex |
⊢ 𝑓 ∈ V |
11 |
10
|
elixp |
⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) |
12 |
10
|
elixp |
⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
13 |
11 12
|
anbi12i |
⊢ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) ↔ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ) |
14 |
10
|
elixp |
⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) ) |
15 |
9 13 14
|
3bitr4i |
⊢ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) ↔ 𝑓 ∈ X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ) |
16 |
15
|
ineqri |
⊢ ( X 𝑥 ∈ 𝐴 𝐵 ∩ X 𝑥 ∈ 𝐴 𝐶 ) = X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) |