Metamath Proof Explorer

Theorem csbuni

Description: Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012) (Revised by NM, 22-Aug-2018)

Ref Expression
Assertion csbuni 
|- [_ A / x ]_ U. B = U. [_ A / x ]_ B

Proof

Step Hyp Ref Expression
1 csbab 
 |-  [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) }
2 sbcex2 
 |-  ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) )
3 sbcan 
 |-  ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) )
4 sbcg 
 |-  ( A e. _V -> ( [. A / x ]. z e. y <-> z e. y ) )
5 4 anbi1d 
 |-  ( A e. _V -> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ [. A / x ]. y e. B ) ) )
6 sbcel2 
 |-  ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B )
7 6 anbi2i 
 |-  ( ( z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) )
8 5 7 bitrdi 
 |-  ( A e. _V -> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) )
9 3 8 bitrid 
 |-  ( A e. _V -> ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) )
10 9 exbidv 
 |-  ( A e. _V -> ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) )
11 2 10 bitrid 
 |-  ( A e. _V -> ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) )
12 11 abbidv 
 |-  ( A e. _V -> { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } )
13 1 12 eqtrid 
 |-  ( A e. _V -> [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } )
14 df-uni 
 |-  U. B = { z | E. y ( z e. y /\ y e. B ) }
15 14 csbeq2i 
 |-  [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) }
16 df-uni 
 |-  U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) }
17 13 15 16 3eqtr4g 
 |-  ( A e. _V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B )
18 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ U. B = (/) )
19 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
20 19 unieqd 
 |-  ( -. A e. _V -> U. [_ A / x ]_ B = U. (/) )
21 uni0 
 |-  U. (/) = (/)
22 20 21 eqtr2di 
 |-  ( -. A e. _V -> (/) = U. [_ A / x ]_ B )
23 18 22 eqtrd 
 |-  ( -. A e. _V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B )
24 17 23 pm2.61i 
 |-  [_ A / x ]_ U. B = U. [_ A / x ]_ B