Metamath Proof Explorer

Theorem csbxp

Description: Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012) (Revised by NM, 23-Aug-2018)

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

Proof

Step Hyp Ref Expression
1 csbab 
 |-  [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
2 sbcex2 
 |-  ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) )
3 sbcex2 
 |-  ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) )
4 sbcan 
 |-  ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) )
5 sbcg 
 |-  ( A e. _V -> ( [. A / x ]. z = <. w , y >. <-> z = <. w , y >. ) )
6 sbcan 
 |-  ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) )
7 sbcel2 
 |-  ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B )
8 sbcel2 
 |-  ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C )
9 7 8 anbi12i 
 |-  ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) )
10 6 9 bitri 
 |-  ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) )
11 10 a1i 
 |-  ( A e. _V -> ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
12 5 11 anbi12d 
 |-  ( A e. _V -> ( ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) )
13 sbcex 
 |-  ( [. A / x ]. ( w e. B /\ y e. C ) -> A e. _V )
14 13 con3i 
 |-  ( -. A e. _V -> -. [. A / x ]. ( w e. B /\ y e. C ) )
15 14 intnand 
 |-  ( -. A e. _V -> -. ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) )
16 noel 
 |-  -. y e. (/)
17 16 a1i 
 |-  ( -. A e. _V -> -. y e. (/) )
18 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ C = (/) )
19 17 18 neleqtrrd 
 |-  ( -. A e. _V -> -. y e. [_ A / x ]_ C )
20 19 intnand 
 |-  ( -. A e. _V -> -. ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) )
21 20 intnand 
 |-  ( -. A e. _V -> -. ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
22 15 21 2falsed 
 |-  ( -. A e. _V -> ( ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) )
23 12 22 pm2.61i 
 |-  ( ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
24 4 23 bitri 
 |-  ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
25 24 exbii 
 |-  ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
26 3 25 bitri 
 |-  ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
27 26 exbii 
 |-  ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
28 2 27 bitri 
 |-  ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
29 28 abbii 
 |-  { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
30 1 29 eqtri 
 |-  [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
31 df-xp 
 |-  ( B X. C ) = { <. w , y >. | ( w e. B /\ y e. C ) }
32 df-opab 
 |-  { <. w , y >. | ( w e. B /\ y e. C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
33 31 32 eqtri 
 |-  ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
34 33 csbeq2i 
 |-  [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
35 df-xp 
 |-  ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { <. w , y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) }
36 df-opab 
 |-  { <. w , y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
37 35 36 eqtri 
 |-  ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
38 30 34 37 3eqtr4i 
 |-  [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C )