Step |
Hyp |
Ref |
Expression |
1 |
|
r19.28zv |
⊢ ( 𝐵 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐵 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ) |
2 |
|
eliin |
⊢ ( 𝑓 ∈ V → ( 𝑓 ∈ ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) ) |
3 |
2
|
elv |
⊢ ( 𝑓 ∈ ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) |
4 |
|
vex |
⊢ 𝑓 ∈ V |
5 |
4
|
elixp |
⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
6 |
5
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝐵 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
7 |
3 6
|
bitri |
⊢ ( 𝑓 ∈ ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
8 |
4
|
elixp |
⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ) ) |
9 |
|
fvex |
⊢ ( 𝑓 ‘ 𝑥 ) ∈ V |
10 |
|
eliin |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ( ( 𝑓 ‘ 𝑥 ) ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
11 |
9 10
|
ax-mp |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) |
12 |
11
|
ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) |
13 |
|
ralcom |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) |
14 |
12 13
|
bitri |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) |
15 |
14
|
anbi2i |
⊢ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
16 |
8 15
|
bitri |
⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) |
17 |
1 7 16
|
3bitr4g |
⊢ ( 𝐵 ≠ ∅ → ( 𝑓 ∈ ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝐶 ↔ 𝑓 ∈ X 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ) ) |
18 |
17
|
eqrdv |
⊢ ( 𝐵 ≠ ∅ → ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ) |
19 |
18
|
eqcomd |
⊢ ( 𝐵 ≠ ∅ → X 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝐶 ) |