Theorem sbc19.21g

Description: Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004)

	Ref	Expression
Hypothesis	sbcgf.1	$$⊢Ⅎx\phi$$
Assertion	sbc19.21g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcgf.1	$$⊢Ⅎx\phi$$
2		sbcimg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \to \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)\right)$$
3	1	sbcgf	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
4	3	imbi1d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)\right)$$
5	2 4	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)\right)$$