Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1534.1 |
⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) } |
2 |
|
bnj1534.2 |
⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 ) |
3 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐴 |
4 |
|
nfcv |
⊢ Ⅎ 𝑧 𝐴 |
5 |
|
nfv |
⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) |
6 |
2
|
nfcii |
⊢ Ⅎ 𝑥 𝐹 |
7 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑧 |
8 |
6 7
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) |
9 |
|
nfcv |
⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑧 ) |
10 |
8 9
|
nfne |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) |
11 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) ) |
12 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑧 ) ) |
13 |
11 12
|
neeq12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) ) ) |
14 |
3 4 5 10 13
|
cbvrabw |
⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) } = { 𝑧 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) } |
15 |
1 14
|
eqtri |
⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) } |