Step |
Hyp |
Ref |
Expression |
1 |
|
ac6s.1 |
⊢ 𝐴 ∈ V |
2 |
|
ac6s.2 |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) |
3 |
2
|
notbid |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) |
4 |
1 3
|
ac6s |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) ) |
5 |
4
|
con3i |
⊢ ( ¬ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) → ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 ) |
6 |
|
dfrex2 |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) |
7 |
6
|
imbi2i |
⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 → ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) ) |
8 |
7
|
albii |
⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) ) |
9 |
|
alinexa |
⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) ↔ ¬ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) ) |
10 |
8 9
|
bitri |
⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ¬ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) ) |
11 |
|
dfral2 |
⊢ ( ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 ) |
12 |
11
|
rexbii |
⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 ) |
13 |
|
rexnal |
⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 ) |
14 |
12 13
|
bitri |
⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 ) |
15 |
5 10 14
|
3imtr4i |
⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ) |