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 )