Theorem bnj62

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

	Ref	Expression
Assertion	bnj62	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}xFnA\leftrightarrow zFnA$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2		fneq1	$$⊢x=y\to \left(xFnA\leftrightarrow yFnA\right)$$
3	1 2	sbcie	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}xFnA\leftrightarrow yFnA$$
4	3	sbcbii	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}xFnA\leftrightarrow \underset{\dot{}}{[}z/y\underset{\dot{}}{]}yFnA$$
5		sbccow	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}xFnA\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}xFnA$$
6		vex	$$⊢z\in \mathrm{V}$$
7		fneq1	$$⊢y=z\to \left(yFnA\leftrightarrow zFnA\right)$$
8	6 7	sbcie	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}yFnA\leftrightarrow zFnA$$
9	4 5 8	3bitr3i	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}xFnA\leftrightarrow zFnA$$