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 φ$
	Assertion	sbc19.21g	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} (φ \to ψ) \leftrightarrow (φ \to \underset{˙}{[} A / x \underset{˙}{]} ψ))$

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

Metamath Proof Explorer