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 𝐴 / 𝑥 ( 𝐵 × 𝐶 ) = ( 𝐴 / 𝑥 𝐵 × 𝐴 / 𝑥 𝐶 )

Proof

Step Hyp Ref Expression
1 csbab 𝐴 / 𝑥 { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) } = { 𝑧[ 𝐴 / 𝑥 ]𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) }
2 sbcex2 ( [ 𝐴 / 𝑥 ]𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ]𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) )
3 sbcex2 ( [ 𝐴 / 𝑥 ]𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) )
4 sbcan ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) ) )
5 sbcg ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ) )
6 sbcan ( [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤𝐵[ 𝐴 / 𝑥 ] 𝑦𝐶 ) )
7 sbcel2 ( [ 𝐴 / 𝑥 ] 𝑤𝐵𝑤 𝐴 / 𝑥 𝐵 )
8 sbcel2 ( [ 𝐴 / 𝑥 ] 𝑦𝐶𝑦 𝐴 / 𝑥 𝐶 )
9 7 8 anbi12i ( ( [ 𝐴 / 𝑥 ] 𝑤𝐵[ 𝐴 / 𝑥 ] 𝑦𝐶 ) ↔ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) )
10 6 9 bitri ( [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) ↔ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) )
11 10 a1i ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) ↔ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
12 5 11 anbi12d ( 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) ) )
13 sbcex ( [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) → 𝐴 ∈ V )
14 13 con3i ( ¬ 𝐴 ∈ V → ¬ [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) )
15 14 intnand ( ¬ 𝐴 ∈ V → ¬ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) ) )
16 noel ¬ 𝑦 ∈ ∅
17 16 a1i ( ¬ 𝐴 ∈ V → ¬ 𝑦 ∈ ∅ )
18 csbprc ( ¬ 𝐴 ∈ V → 𝐴 / 𝑥 𝐶 = ∅ )
19 17 18 neleqtrrd ( ¬ 𝐴 ∈ V → ¬ 𝑦 𝐴 / 𝑥 𝐶 )
20 19 intnand ( ¬ 𝐴 ∈ V → ¬ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) )
21 20 intnand ( ¬ 𝐴 ∈ V → ¬ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
22 15 21 2falsed ( ¬ 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) ) )
23 12 22 pm2.61i ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤𝐵𝑦𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
24 4 23 bitri ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
25 24 exbii ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
26 3 25 bitri ( [ 𝐴 / 𝑥 ]𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
27 26 exbii ( ∃ 𝑤 [ 𝐴 / 𝑥 ]𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) ↔ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
28 2 27 bitri ( [ 𝐴 / 𝑥 ]𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) ↔ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
29 28 abbii { 𝑧[ 𝐴 / 𝑥 ]𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) }
30 1 29 eqtri 𝐴 / 𝑥 { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) }
31 df-xp ( 𝐵 × 𝐶 ) = { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤𝐵𝑦𝐶 ) }
32 df-opab { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤𝐵𝑦𝐶 ) } = { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) }
33 31 32 eqtri ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) }
34 33 csbeq2i 𝐴 / 𝑥 ( 𝐵 × 𝐶 ) = 𝐴 / 𝑥 { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤𝐵𝑦𝐶 ) ) }
35 df-xp ( 𝐴 / 𝑥 𝐵 × 𝐴 / 𝑥 𝐶 ) = { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) }
36 df-opab { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) } = { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) }
37 35 36 eqtri ( 𝐴 / 𝑥 𝐵 × 𝐴 / 𝑥 𝐶 ) = { 𝑧 ∣ ∃ 𝑤𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) }
38 30 34 37 3eqtr4i 𝐴 / 𝑥 ( 𝐵 × 𝐶 ) = ( 𝐴 / 𝑥 𝐵 × 𝐴 / 𝑥 𝐶 )