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 xw\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 xw\in F$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}zA$$
5		nfv	$$⊢ℲzF\left(x\right)\ne H\left(x\right)$$
6	2	nfcii	$$⊢\underset{\_}{Ⅎ}xF$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
8	6 7	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(z\right)$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xH\left(z\right)$$
10	8 9	nfne	$$⊢ℲxF\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)\leftrightarrow 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\}$$