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 ⊢ [˙A / x]˙ B ∈ C ↔ B ∈ ⦋ A / x⦌ C

Proof

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