This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvrabcsfw

Description: Version of cbvrabcsf with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (Revised by GG, 26-Jan-2024)

Ref Expression
Hypotheses cbvrabcsfw.1 ⊢ Ⅎ 𝑦 𝐴
cbvrabcsfw.2 ⊢ Ⅎ 𝑥 𝐵
cbvrabcsfw.3 ⊢ Ⅎ 𝑦 𝜑
cbvrabcsfw.4 ⊢ Ⅎ 𝑥 𝜓
cbvrabcsfw.5 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
cbvrabcsfw.6 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion cbvrabcsfw { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ 𝜓 }

Proof

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 ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ 𝜓 }