Theorem bnj1468

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1468.1	$$⊢\psi \to \forall x\psi$$
	bnj1468.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	bnj1468.3	$$⊢y\in A\to \forall xy\in A$$
Assertion	bnj1468	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj1468.1	$$⊢\psi \to \forall x\psi$$
2		bnj1468.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
3		bnj1468.3	$$⊢y\in A\to \forall xy\in A$$
4		sbccow	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
5		ax-5	$$⊢\psi \to \forall y\psi$$
6	3	nfcii	$$⊢\underset{\_}{Ⅎ}xA$$
7	6	nfeq2	$$⊢Ⅎxy=A$$
8		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
9	1	nf5i	$$⊢Ⅎx\psi$$
10	8 9	nfbi	$$⊢Ⅎx\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
11	7 10	nfim	$$⊢Ⅎx\left(y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)$$
12	11	nf5ri	$$⊢\left(y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)\to \forall x\left(y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)$$
13		ax6ev	$$⊢\exists xx=y$$
14		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
15	14 2	syl6bir	$$⊢x=y\to \left(y=A\to \left(\phi \leftrightarrow \psi \right)\right)$$
16		sbceq1a	$$⊢x=y\to \left(\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
17	16	bibi1d	$$⊢x=y\to \left(\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)$$
18	15 17	sylibd	$$⊢x=y\to \left(y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)$$
19	13 18	bnj101	$$⊢\exists x\left(y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)$$
20	12 19	bnj1131	$$⊢y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
21	5 20	bnj1464	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
22	4 21	bitr3id	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$