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 e. C <-> B e. [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 sbcel12
 |-  ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C )
2 csbconstg
 |-  ( A e. _V -> [_ A / x ]_ B = B )
3 2 eleq1d
 |-  ( A e. _V -> ( [_ A / x ]_ B e. [_ A / x ]_ C <-> B e. [_ A / x ]_ C ) )
4 1 3 syl5bb
 |-  ( A e. _V -> ( [. A / x ]. B e. C <-> B e. [_ A / x ]_ C ) )
5 sbcex
 |-  ( [. A / x ]. B e. C -> A e. _V )
6 5 con3i
 |-  ( -. A e. _V -> -. [. A / x ]. B e. C )
7 noel
 |-  -. B e. (/)
8 csbprc
 |-  ( -. A e. _V -> [_ A / x ]_ C = (/) )
9 8 eleq2d
 |-  ( -. A e. _V -> ( B e. [_ A / x ]_ C <-> B e. (/) ) )
10 7 9 mtbiri
 |-  ( -. A e. _V -> -. B e. [_ A / x ]_ C )
11 6 10 2falsed
 |-  ( -. A e. _V -> ( [. A / x ]. B e. C <-> B e. [_ A / x ]_ C ) )
12 4 11 pm2.61i
 |-  ( [. A / x ]. B e. C <-> B e. [_ A / x ]_ C )