Theorem sbcnel12g

Description: Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011)

	Ref	Expression
Assertion	sbcnel12g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 ∉ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∉ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		sbcng	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ¬ 𝐵 ∈ 𝐶 ↔ ¬ [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ) )
2		df-nel	⊢ ( 𝐵 ∉ 𝐶 ↔ ¬ 𝐵 ∈ 𝐶 )
3	2	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∉ 𝐶 ↔ [ 𝐴 / 𝑥 ] ¬ 𝐵 ∈ 𝐶 )
4		df-nel	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∉ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
5		sbcel12	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
6	4 5	xchbinxr	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∉ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ¬ [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 )
7	1 3 6	3bitr4g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 ∉ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∉ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )