Theorem sbcel2

Description: Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbcel2	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		sbcel12	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
2		csbconstg	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 )
3	2	eleq1d	⊢ ( 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
4	1 3	bitrid	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
5		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 → 𝐴 ∈ V )
6	5	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 )
7		noel	⊢ ¬ 𝐵 ∈ ∅
8		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ∅ )
9	8	eleq2d	⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝐵 ∈ ∅ ) )
10	7 9	mtbiri	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
11	6 10	2falsed	⊢ ( ¬ 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
12	4 11	pm2.61i	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )