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

Metamath Proof Explorer

Theorem cbvrabwOLD

Description: Obsolete version of cbvrabw as of 19-Jul-2025. (Contributed by Andrew Salmon, 11-Jul-2011) Avoid ax-13 . (Revised by GG, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cbvrabw.1 
|- F/_ x A
cbvrabw.2 
|- F/_ y A
cbvrabw.3 
|- F/ y ph
cbvrabw.4 
|- F/ x ps
cbvrabw.5 
|- ( x = y -> ( ph <-> ps ) )
Assertion cbvrabwOLD 
|- { x e. A | ph } = { y e. A | ps }

Proof

Step Hyp Ref Expression
1 cbvrabw.1 
 |-  F/_ x A
2 cbvrabw.2 
 |-  F/_ y A
3 cbvrabw.3 
 |-  F/ y ph
4 cbvrabw.4 
 |-  F/ x ps
5 cbvrabw.5 
 |-  ( x = y -> ( ph <-> ps ) )
6 nfv 
 |-  F/ z ( x e. A /\ ph )
7 1 nfcri 
 |-  F/ x z e. A
8 nfs1v 
 |-  F/ x [ z / x ] ph
9 7 8 nfan 
 |-  F/ x ( z e. A /\ [ z / x ] ph )
10 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
11 sbequ12 
 |-  ( x = z -> ( ph <-> [ z / x ] ph ) )
12 10 11 anbi12d 
 |-  ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. A /\ [ z / x ] ph ) ) )
13 6 9 12 cbvabw 
 |-  { x | ( x e. A /\ ph ) } = { z | ( z e. A /\ [ z / x ] ph ) }
14 2 nfcri 
 |-  F/ y z e. A
15 3 nfsbv 
 |-  F/ y [ z / x ] ph
16 14 15 nfan 
 |-  F/ y ( z e. A /\ [ z / x ] ph )
17 nfv 
 |-  F/ z ( y e. A /\ ps )
18 eleq1w 
 |-  ( z = y -> ( z e. A <-> y e. A ) )
19 sbequ 
 |-  ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
20 4 5 sbiev 
 |-  ( [ y / x ] ph <-> ps )
21 19 20 bitrdi 
 |-  ( z = y -> ( [ z / x ] ph <-> ps ) )
22 18 21 anbi12d 
 |-  ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
23 16 17 22 cbvabw 
 |-  { z | ( z e. A /\ [ z / x ] ph ) } = { y | ( y e. A /\ ps ) }
24 13 23 eqtri 
 |-  { x | ( x e. A /\ ph ) } = { y | ( y e. A /\ ps ) }
25 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
26 df-rab 
 |-  { y e. A | ps } = { y | ( y e. A /\ ps ) }
27 24 25 26 3eqtr4i 
 |-  { x e. A | ph } = { y e. A | ps }