# Metamath Proof Explorer

## Theorem bnj1534

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1534.1 ${⊢}{D}=\left\{{x}\in {A}|{F}\left({x}\right)\ne {H}\left({x}\right)\right\}$
bnj1534.2 ${⊢}{w}\in {F}\to \forall {x}\phantom{\rule{.4em}{0ex}}{w}\in {F}$
Assertion bnj1534 ${⊢}{D}=\left\{{z}\in {A}|{F}\left({z}\right)\ne {H}\left({z}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 bnj1534.1 ${⊢}{D}=\left\{{x}\in {A}|{F}\left({x}\right)\ne {H}\left({x}\right)\right\}$
2 bnj1534.2 ${⊢}{w}\in {F}\to \forall {x}\phantom{\rule{.4em}{0ex}}{w}\in {F}$
3 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
4 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{A}$
5 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\ne {H}\left({x}\right)$
6 2 nfcii ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
7 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
8 6 7 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)$
9 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{H}\left({z}\right)$
10 8 9 nfne ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)\ne {H}\left({z}\right)$
11 fveq2 ${⊢}{x}={z}\to {F}\left({x}\right)={F}\left({z}\right)$
12 fveq2 ${⊢}{x}={z}\to {H}\left({x}\right)={H}\left({z}\right)$
13 11 12 neeq12d ${⊢}{x}={z}\to \left({F}\left({x}\right)\ne {H}\left({x}\right)↔{F}\left({z}\right)\ne {H}\left({z}\right)\right)$
14 3 4 5 10 13 cbvrabw ${⊢}\left\{{x}\in {A}|{F}\left({x}\right)\ne {H}\left({x}\right)\right\}=\left\{{z}\in {A}|{F}\left({z}\right)\ne {H}\left({z}\right)\right\}$
15 1 14 eqtri ${⊢}{D}=\left\{{z}\in {A}|{F}\left({z}\right)\ne {H}\left({z}\right)\right\}$