Metamath Proof Explorer


Theorem cbvrabw

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvrabw.1 𝑥 𝐴
cbvrabw.2 𝑦 𝐴
cbvrabw.3 𝑦 𝜑
cbvrabw.4 𝑥 𝜓
cbvrabw.5 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cbvrabw { 𝑥𝐴𝜑 } = { 𝑦𝐴𝜓 }

Proof

Step Hyp Ref Expression
1 cbvrabw.1 𝑥 𝐴
2 cbvrabw.2 𝑦 𝐴
3 cbvrabw.3 𝑦 𝜑
4 cbvrabw.4 𝑥 𝜓
5 cbvrabw.5 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
6 nfv 𝑧 ( 𝑥𝐴𝜑 )
7 1 nfcri 𝑥 𝑧𝐴
8 nfs1v 𝑥 [ 𝑧 / 𝑥 ] 𝜑
9 7 8 nfan 𝑥 ( 𝑧𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
10 eleq1w ( 𝑥 = 𝑧 → ( 𝑥𝐴𝑧𝐴 ) )
11 sbequ12 ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
12 10 11 anbi12d ( 𝑥 = 𝑧 → ( ( 𝑥𝐴𝜑 ) ↔ ( 𝑧𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
13 6 9 12 cbvabw { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = { 𝑧 ∣ ( 𝑧𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) }
14 2 nfcri 𝑦 𝑧𝐴
15 3 nfsbv 𝑦 [ 𝑧 / 𝑥 ] 𝜑
16 14 15 nfan 𝑦 ( 𝑧𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
17 nfv 𝑧 ( 𝑦𝐴𝜓 )
18 eleq1w ( 𝑧 = 𝑦 → ( 𝑧𝐴𝑦𝐴 ) )
19 sbequ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
20 4 5 sbiev ( [ 𝑦 / 𝑥 ] 𝜑𝜓 )
21 19 20 bitrdi ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑𝜓 ) )
22 18 21 anbi12d ( 𝑧 = 𝑦 → ( ( 𝑧𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦𝐴𝜓 ) ) )
23 16 17 22 cbvabw { 𝑧 ∣ ( 𝑧𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) } = { 𝑦 ∣ ( 𝑦𝐴𝜓 ) }
24 13 23 eqtri { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = { 𝑦 ∣ ( 𝑦𝐴𝜓 ) }
25 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
26 df-rab { 𝑦𝐴𝜓 } = { 𝑦 ∣ ( 𝑦𝐴𝜓 ) }
27 24 25 26 3eqtr4i { 𝑥𝐴𝜑 } = { 𝑦𝐴𝜓 }