Theorem csbxp 5200

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

Assertion

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

Proof of Theorem csbxp

Dummy variables w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbab 4008	. . 3 |- [_ 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 3486	. . . . 5 |- ( [. 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 3486	. . . . . . 7 |- ( [. 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 3478	. . . . . . . . 9 |- ( [. 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 3503	. . . . . . . . . . 11 |- ( A e. _V -> ( [. A / x ]. z = <. w , y >. <-> z = <. w , y >. ) )
6		sbcan 3478	. . . . . . . . . . . . 13 |- ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) )
7		sbcel2 3989	. . . . . . . . . . . . . 14 |- ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B )
8		sbcel2 3989	. . . . . . . . . . . . . 14 |- ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C )
9	7, 8	anbi12i 733	. . . . . . . . . . . . 13 |- ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) )
10	6, 9	bitri 264	. . . . . . . . . . . 12 |- ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) )
11	10	a1i 11	. . . . . . . . . . 11 |- ( 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 747	. . . . . . . . . 10 |- ( 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 3445	. . . . . . . . . . . . 13 |- ( [. A / x ]. ( w e. B /\ y e. C ) -> A e. _V )
14	13	con3i 150	. . . . . . . . . . . 12 |- ( -. A e. _V -> -. [. A / x ]. ( w e. B /\ y e. C ) )
15	14	intnand 962	. . . . . . . . . . 11 |- ( -. A e. _V -> -. ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) )
16		noel 3919	. . . . . . . . . . . . . . 15 |- -. y e. (/)
17	16	a1i 11	. . . . . . . . . . . . . 14 |- ( -. A e. _V -> -. y e. (/) )
18		csbprc 3980	. . . . . . . . . . . . . 14 |- ( -. A e. _V -> [_ A / x ]_ C = (/) )
19	17, 18	neleqtrrd 2723	. . . . . . . . . . . . 13 |- ( -. A e. _V -> -. y e. [_ A / x ]_ C )
20	19	intnand 962	. . . . . . . . . . . 12 |- ( -. A e. _V -> -. ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) )
21	20	intnand 962	. . . . . . . . . . 11 |- ( -. A e. _V -> -. ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) )
22	15, 21	2falsed 366	. . . . . . . . . 10 |- ( -. 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 176	. . . . . . . . 9 |- ( ( [. 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 264	. . . . . . . 8 |- ( [. 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 1774	. . . . . . 7 |- ( 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 264	. . . . . 6 |- ( [. 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 1774	. . . . 5 |- ( 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 264	. . . 4 |- ( [. 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 2739	. . 3 |- { 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 2644	. 2 |- [_ 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 5120	. . . 4 |- ( B X. C ) = { <. w , y >. | ( w e. B /\ y e. C ) }
32		df-opab 4713	. . . 4 |- { <. 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 2644	. . 3 |- ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
34	33	csbeq2i 3993	. 2 |- [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
35		df-xp 5120	. . 3 |- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { <. w , y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) }
36		df-opab 4713	. . 3 |- { <. 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 2644	. 2 |- ( [_ 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 2654	1 |- [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   _Vcvv 3200   [.wsbc 3435   [_csb 3533   (/)c0 3915   <.cop 4183   {copab 4712   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-nul 3916  df-opab 4713  df-xp 5120

This theorem is referenced by:  csbres  5399  csbfinxpg  33225  disjxp1  39238