Step |
Hyp |
Ref |
Expression |
1 |
|
cbvrabcsfw.1 |
⊢ Ⅎ 𝑦 𝐴 |
2 |
|
cbvrabcsfw.2 |
⊢ Ⅎ 𝑥 𝐵 |
3 |
|
cbvrabcsfw.3 |
⊢ Ⅎ 𝑦 𝜑 |
4 |
|
cbvrabcsfw.4 |
⊢ Ⅎ 𝑥 𝜓 |
5 |
|
cbvrabcsfw.5 |
⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 ) |
6 |
|
cbvrabcsfw.6 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) |
7 |
|
nfv |
⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) |
8 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐴 |
9 |
8
|
nfcri |
⊢ Ⅎ 𝑥 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 |
10 |
|
nfs1v |
⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑 |
11 |
9 10
|
nfan |
⊢ Ⅎ 𝑥 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) |
12 |
|
id |
⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 ) |
13 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑧 → 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) |
14 |
12 13
|
eleq12d |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) ) |
15 |
|
sbequ12 |
⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) ) |
16 |
14 15
|
anbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) ) |
17 |
7 11 16
|
cbvabw |
⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑧 ∣ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) } |
18 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑧 |
19 |
18 1
|
nfcsbw |
⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ 𝐴 |
20 |
19
|
nfcri |
⊢ Ⅎ 𝑦 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 |
21 |
3
|
nfsbv |
⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 |
22 |
20 21
|
nfan |
⊢ Ⅎ 𝑦 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) |
23 |
|
nfv |
⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) |
24 |
|
id |
⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 ) |
25 |
|
csbeq1 |
⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) |
26 |
|
vex |
⊢ 𝑦 ∈ V |
27 |
26 2 5
|
csbief |
⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐵 |
28 |
25 27
|
eqtrdi |
⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = 𝐵 ) |
29 |
24 28
|
eleq12d |
⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ↔ 𝑦 ∈ 𝐵 ) ) |
30 |
4 6
|
sbhypf |
⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) ) |
31 |
29 30
|
anbi12d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ) |
32 |
22 23 31
|
cbvabw |
⊢ { 𝑧 ∣ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) } |
33 |
17 32
|
eqtri |
⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) } |
34 |
|
df-rab |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
35 |
|
df-rab |
⊢ { 𝑦 ∈ 𝐵 ∣ 𝜓 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) } |
36 |
33 34 35
|
3eqtr4i |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ 𝜓 } |