Metamath Proof Explorer


Theorem cbvrabcsf

Description: A more general version of cbvrab with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvralcsf.1 𝑦 𝐴
2 cbvralcsf.2 𝑥 𝐵
3 cbvralcsf.3 𝑦 𝜑
4 cbvralcsf.4 𝑥 𝜓
5 cbvralcsf.5 ( 𝑥 = 𝑦𝐴 = 𝐵 )
6 cbvralcsf.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 cbvab { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = { 𝑧 ∣ ( 𝑧 𝑧 / 𝑥 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) }
18 nfcv 𝑦 𝑧
19 18 1 nfcsb 𝑦 𝑧 / 𝑥 𝐴
20 19 nfcri 𝑦 𝑧 𝑧 / 𝑥 𝐴
21 3 nfsb 𝑦 [ 𝑧 / 𝑥 ] 𝜑
22 20 21 nfan 𝑦 ( 𝑧 𝑧 / 𝑥 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
23 nfv 𝑧 ( 𝑦𝐵𝜓 )
24 id ( 𝑧 = 𝑦𝑧 = 𝑦 )
25 csbeq1 ( 𝑧 = 𝑦 𝑧 / 𝑥 𝐴 = 𝑦 / 𝑥 𝐴 )
26 df-csb 𝑦 / 𝑥 𝐴 = { 𝑣[ 𝑦 / 𝑥 ] 𝑣𝐴 }
27 2 nfcri 𝑥 𝑣𝐵
28 5 eleq2d ( 𝑥 = 𝑦 → ( 𝑣𝐴𝑣𝐵 ) )
29 27 28 sbie ( [ 𝑦 / 𝑥 ] 𝑣𝐴𝑣𝐵 )
30 sbsbc ( [ 𝑦 / 𝑥 ] 𝑣𝐴[ 𝑦 / 𝑥 ] 𝑣𝐴 )
31 29 30 bitr3i ( 𝑣𝐵[ 𝑦 / 𝑥 ] 𝑣𝐴 )
32 31 abbi2i 𝐵 = { 𝑣[ 𝑦 / 𝑥 ] 𝑣𝐴 }
33 26 32 eqtr4i 𝑦 / 𝑥 𝐴 = 𝐵
34 25 33 eqtrdi ( 𝑧 = 𝑦 𝑧 / 𝑥 𝐴 = 𝐵 )
35 24 34 eleq12d ( 𝑧 = 𝑦 → ( 𝑧 𝑧 / 𝑥 𝐴𝑦𝐵 ) )
36 sbequ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
37 4 6 sbie ( [ 𝑦 / 𝑥 ] 𝜑𝜓 )
38 36 37 bitrdi ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑𝜓 ) )
39 35 38 anbi12d ( 𝑧 = 𝑦 → ( ( 𝑧 𝑧 / 𝑥 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦𝐵𝜓 ) ) )
40 22 23 39 cbvab { 𝑧 ∣ ( 𝑧 𝑧 / 𝑥 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) } = { 𝑦 ∣ ( 𝑦𝐵𝜓 ) }
41 17 40 eqtri { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = { 𝑦 ∣ ( 𝑦𝐵𝜓 ) }
42 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
43 df-rab { 𝑦𝐵𝜓 } = { 𝑦 ∣ ( 𝑦𝐵𝜓 ) }
44 41 42 43 3eqtr4i { 𝑥𝐴𝜑 } = { 𝑦𝐵𝜓 }