Metamath Proof Explorer

Theorem sbcel12

Description: Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion sbcel12 
|- ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] B e. C <-> [. A / x ]. B e. C ) )
2 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] y e. B <-> [. A / x ]. y e. B ) )
3 2 abbidv 
 |-  ( z = A -> { y | [ z / x ] y e. B } = { y | [. A / x ]. y e. B } )
4 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] y e. C <-> [. A / x ]. y e. C ) )
5 4 abbidv 
 |-  ( z = A -> { y | [ z / x ] y e. C } = { y | [. A / x ]. y e. C } )
6 3 5 eleq12d 
 |-  ( z = A -> ( { y | [ z / x ] y e. B } e. { y | [ z / x ] y e. C } <-> { y | [. A / x ]. y e. B } e. { y | [. A / x ]. y e. C } ) )
7 nfs1v 
 |-  F/ x [ z / x ] y e. B
8 7 nfab 
 |-  F/_ x { y | [ z / x ] y e. B }
9 nfs1v 
 |-  F/ x [ z / x ] y e. C
10 9 nfab 
 |-  F/_ x { y | [ z / x ] y e. C }
11 8 10 nfel 
 |-  F/ x { y | [ z / x ] y e. B } e. { y | [ z / x ] y e. C }
12 sbab 
 |-  ( x = z -> B = { y | [ z / x ] y e. B } )
13 sbab 
 |-  ( x = z -> C = { y | [ z / x ] y e. C } )
14 12 13 eleq12d 
 |-  ( x = z -> ( B e. C <-> { y | [ z / x ] y e. B } e. { y | [ z / x ] y e. C } ) )
15 11 14 sbiev 
 |-  ( [ z / x ] B e. C <-> { y | [ z / x ] y e. B } e. { y | [ z / x ] y e. C } )
16 1 6 15 vtoclbg 
 |-  ( A e. _V -> ( [. A / x ]. B e. C <-> { y | [. A / x ]. y e. B } e. { y | [. A / x ]. y e. C } ) )
17 df-csb 
 |-  [_ A / x ]_ B = { y | [. A / x ]. y e. B }
18 df-csb 
 |-  [_ A / x ]_ C = { y | [. A / x ]. y e. C }
19 17 18 eleq12i 
 |-  ( [_ A / x ]_ B e. [_ A / x ]_ C <-> { y | [. A / x ]. y e. B } e. { y | [. A / x ]. y e. C } )
20 16 19 bitr4di 
 |-  ( A e. _V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C ) )
21 sbcex 
 |-  ( [. A / x ]. B e. C -> A e. _V )
22 21 con3i 
 |-  ( -. A e. _V -> -. [. A / x ]. B e. C )
23 noel 
 |-  -. [_ A / x ]_ B e. (/)
24 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ C = (/) )
25 24 eleq2d 
 |-  ( -. A e. _V -> ( [_ A / x ]_ B e. [_ A / x ]_ C <-> [_ A / x ]_ B e. (/) ) )
26 23 25 mtbiri 
 |-  ( -. A e. _V -> -. [_ A / x ]_ B e. [_ A / x ]_ C )
27 22 26 2falsed 
 |-  ( -. A e. _V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C ) )
28 20 27 pm2.61i 
 |-  ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C )