Theorem spcdvw

Description: A version of spcdv where ps and ch are direct substitutions of each other. This theorem is useful because it does not require ph and x to be distinct variables. (Contributed by Emmett Weisz, 12-Apr-2020)

	Ref	Expression
Hypotheses	spcdvw.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	spcdvw.2	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
Assertion	spcdvw	⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		spcdvw.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2		spcdvw.2	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
3	2	biimpd	⊢ ( 𝑥 = 𝐴 → ( 𝜓 → 𝜒 ) )
4	3	ax-gen	⊢ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓 → 𝜒 ) )
5		nfv	⊢ Ⅎ 𝑥 𝜒
6		nfcv	⊢ Ⅎ 𝑥 𝐴
7	5 6	spcimgfi1	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓 → 𝜒 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜓 → 𝜒 ) ) )
8	4 1 7	mpsyl	⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 → 𝜒 ) )