This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )