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 Gino Giotto, 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 { 𝑥𝐴𝜑 } = { 𝑦𝐵𝜓 }