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 syl5bb
 |-  ( 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 syl5bb
 |-  ( 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