Step |
Hyp |
Ref |
Expression |
1 |
|
cpcoll2d.1 |
⊢ ( 𝜑 → 𝑥 ∈ 𝐴 ) |
2 |
|
cpcoll2d.2 |
⊢ ( 𝜑 → ∃ 𝑦 𝑥 𝐹 𝑦 ) |
3 |
|
breq2 |
⊢ ( 𝑎 = 𝑦 → ( 𝑥 𝐹 𝑎 ↔ 𝑥 𝐹 𝑦 ) ) |
4 |
3
|
cbvexvw |
⊢ ( ∃ 𝑎 𝑥 𝐹 𝑎 ↔ ∃ 𝑦 𝑥 𝐹 𝑦 ) |
5 |
2 4
|
sylibr |
⊢ ( 𝜑 → ∃ 𝑎 𝑥 𝐹 𝑎 ) |
6 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 𝐹 𝑎 ) → 𝑥 ∈ 𝐴 ) |
7 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 𝐹 𝑎 ) → 𝑥 𝐹 𝑎 ) |
8 |
6 7
|
cpcolld |
⊢ ( ( 𝜑 ∧ 𝑥 𝐹 𝑎 ) → ∃ 𝑎 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑎 ) |
9 |
3
|
cbvrexvw |
⊢ ( ∃ 𝑎 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑎 ↔ ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 ) |
10 |
8 9
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑥 𝐹 𝑎 ) → ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 ) |
11 |
5 10
|
exlimddv |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝐹 Coll 𝐴 ) 𝑥 𝐹 𝑦 ) |