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