This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbun

Description: Distribution of class substitution over union of two classes. (Contributed by Drahflow, 23-Sep-2015) (Revised by Mario Carneiro, 11-Dec-2016) (Revised by NM, 13-Sep-2018)

Ref Expression
Assertion csbun 
|- [_ A / x ]_ ( B u. C ) = ( [_ A / x ]_ B u. [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 csbeq1 
 |-  ( y = A -> [_ y / x ]_ ( B u. C ) = [_ A / x ]_ ( B u. C ) )
2 csbeq1 
 |-  ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
3 csbeq1 
 |-  ( y = A -> [_ y / x ]_ C = [_ A / x ]_ C )
4 2 3 uneq12d 
 |-  ( y = A -> ( [_ y / x ]_ B u. [_ y / x ]_ C ) = ( [_ A / x ]_ B u. [_ A / x ]_ C ) )
5 1 4 eqeq12d 
 |-  ( y = A -> ( [_ y / x ]_ ( B u. C ) = ( [_ y / x ]_ B u. [_ y / x ]_ C ) <-> [_ A / x ]_ ( B u. C ) = ( [_ A / x ]_ B u. [_ A / x ]_ C ) ) )
6 vex 
 |-  y e. _V
7 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
9 7 8 nfun 
 |-  F/_ x ( [_ y / x ]_ B u. [_ y / x ]_ C )
10 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
11 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
12 10 11 uneq12d 
 |-  ( x = y -> ( B u. C ) = ( [_ y / x ]_ B u. [_ y / x ]_ C ) )
13 6 9 12 csbief 
 |-  [_ y / x ]_ ( B u. C ) = ( [_ y / x ]_ B u. [_ y / x ]_ C )
14 5 13 vtoclg 
 |-  ( A e. _V -> [_ A / x ]_ ( B u. C ) = ( [_ A / x ]_ B u. [_ A / x ]_ C ) )
15 un0 
 |-  ( (/) u. (/) ) = (/)
16 15 a1i 
 |-  ( -. A e. _V -> ( (/) u. (/) ) = (/) )
17 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
18 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ C = (/) )
19 17 18 uneq12d 
 |-  ( -. A e. _V -> ( [_ A / x ]_ B u. [_ A / x ]_ C ) = ( (/) u. (/) ) )
20 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ ( B u. C ) = (/) )
21 16 19 20 3eqtr4rd 
 |-  ( -. A e. _V -> [_ A / x ]_ ( B u. C ) = ( [_ A / x ]_ B u. [_ A / x ]_ C ) )
22 14 21 pm2.61i 
 |-  [_ A / x ]_ ( B u. C ) = ( [_ A / x ]_ B u. [_ A / x ]_ C )