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 bitrid 
 |-  ( 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 )