Step |
Hyp |
Ref |
Expression |
1 |
|
kqval.2 |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) |
2 |
1
|
kqfval |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = { 𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦 } ) |
3 |
2
|
3adant3 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = { 𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦 } ) |
4 |
1
|
kqfval |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) = { 𝑦 ∈ 𝐽 ∣ 𝐵 ∈ 𝑦 } ) |
5 |
4
|
3adant2 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) = { 𝑦 ∈ 𝐽 ∣ 𝐵 ∈ 𝑦 } ) |
6 |
3 5
|
eqeq12d |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ { 𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦 } = { 𝑦 ∈ 𝐽 ∣ 𝐵 ∈ 𝑦 } ) ) |
7 |
|
rabbi |
⊢ ( ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ↔ 𝐵 ∈ 𝑦 ) ↔ { 𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦 } = { 𝑦 ∈ 𝐽 ∣ 𝐵 ∈ 𝑦 } ) |
8 |
6 7
|
bitr4di |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ↔ 𝐵 ∈ 𝑦 ) ) ) |