Step |
Hyp |
Ref |
Expression |
1 |
|
funimass4 |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) |
2 |
|
ssel |
⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ dom 𝐹 ) ) |
3 |
|
fvimacnv |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ↔ 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) |
4 |
3
|
ex |
⊢ ( Fun 𝐹 → ( 𝑥 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ↔ 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) ) |
5 |
2 4
|
syl9r |
⊢ ( Fun 𝐹 → ( 𝐴 ⊆ dom 𝐹 → ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ↔ 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) ) ) |
6 |
5
|
imp31 |
⊢ ( ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ↔ 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) |
7 |
6
|
ralbidva |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) |
8 |
1 7
|
bitrd |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) |
9 |
|
dfss3 |
⊢ ( 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) |
10 |
8 9
|
bitr4di |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ) ) |