Step |
Hyp |
Ref |
Expression |
1 |
|
ac9.1 |
⊢ 𝐴 ∈ V |
2 |
1
|
ac6s4 |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) |
3 |
|
n0 |
⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) |
4 |
|
vex |
⊢ 𝑓 ∈ V |
5 |
4
|
elixp |
⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) |
6 |
5
|
exbii |
⊢ ( ∃ 𝑓 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) |
7 |
3 6
|
bitr2i |
⊢ ( ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ↔ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) |
8 |
2 7
|
sylib |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) |
9 |
|
ixpn0 |
⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) |
10 |
8 9
|
impbii |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) |