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
|- F/_ y A
cbvrabcsfw.2
|- F/_ x B
cbvrabcsfw.3
|- F/ y ph
cbvrabcsfw.4
|- F/ x ps
cbvrabcsfw.5
|- ( x = y -> A = B )
cbvrabcsfw.6
|- ( x = y -> ( ph <-> ps ) )
Assertion cbvrabcsfw
|- { x e. A | ph } = { y e. B | ps }

Proof

Step Hyp Ref Expression
1 cbvrabcsfw.1
 |-  F/_ y A
2 cbvrabcsfw.2
 |-  F/_ x B
3 cbvrabcsfw.3
 |-  F/ y ph
4 cbvrabcsfw.4
 |-  F/ x ps
5 cbvrabcsfw.5
 |-  ( x = y -> A = B )
6 cbvrabcsfw.6
 |-  ( x = y -> ( ph <-> ps ) )
7 nfv
 |-  F/ z ( x e. A /\ ph )
8 nfcsb1v
 |-  F/_ x [_ z / x ]_ A
9 8 nfcri
 |-  F/ x z e. [_ z / x ]_ A
10 nfs1v
 |-  F/ x [ z / x ] ph
11 9 10 nfan
 |-  F/ x ( z e. [_ z / x ]_ A /\ [ z / x ] ph )
12 id
 |-  ( x = z -> x = z )
13 csbeq1a
 |-  ( x = z -> A = [_ z / x ]_ A )
14 12 13 eleq12d
 |-  ( x = z -> ( x e. A <-> z e. [_ z / x ]_ A ) )
15 sbequ12
 |-  ( x = z -> ( ph <-> [ z / x ] ph ) )
16 14 15 anbi12d
 |-  ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) ) )
17 7 11 16 cbvabw
 |-  { x | ( x e. A /\ ph ) } = { z | ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) }
18 nfcv
 |-  F/_ y z
19 18 1 nfcsbw
 |-  F/_ y [_ z / x ]_ A
20 19 nfcri
 |-  F/ y z e. [_ z / x ]_ A
21 3 nfsbv
 |-  F/ y [ z / x ] ph
22 20 21 nfan
 |-  F/ y ( z e. [_ z / x ]_ A /\ [ z / x ] ph )
23 nfv
 |-  F/ z ( y e. B /\ ps )
24 id
 |-  ( z = y -> z = y )
25 csbeq1
 |-  ( z = y -> [_ z / x ]_ A = [_ y / x ]_ A )
26 vex
 |-  y e. _V
27 26 2 5 csbief
 |-  [_ y / x ]_ A = B
28 25 27 eqtrdi
 |-  ( z = y -> [_ z / x ]_ A = B )
29 24 28 eleq12d
 |-  ( z = y -> ( z e. [_ z / x ]_ A <-> y e. B ) )
30 4 6 sbhypf
 |-  ( z = y -> ( [ z / x ] ph <-> ps ) )
31 29 30 anbi12d
 |-  ( z = y -> ( ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) <-> ( y e. B /\ ps ) ) )
32 22 23 31 cbvabw
 |-  { z | ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) } = { y | ( y e. B /\ ps ) }
33 17 32 eqtri
 |-  { x | ( x e. A /\ ph ) } = { y | ( y e. B /\ ps ) }
34 df-rab
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
35 df-rab
 |-  { y e. B | ps } = { y | ( y e. B /\ ps ) }
36 33 34 35 3eqtr4i
 |-  { x e. A | ph } = { y e. B | ps }