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

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) Avoid ax-13 . (Revised by GG, 10-Jan-2024) Avoid ax-10 . (Revised by Wolf Lammen, 19-Jul-2025)

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 cbvrabw 
|- { 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 2 nfcri 
 |-  F/ y x e. A
7 6 3 nfan 
 |-  F/ y ( x e. A /\ ph )
8 1 nfcri 
 |-  F/ x y e. A
9 8 4 nfan 
 |-  F/ x ( y e. A /\ ps )
10 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
11 10 5 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) )
12 7 9 11 cbvabw 
 |-  { x | ( x e. A /\ ph ) } = { y | ( y e. A /\ ps ) }
13 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
14 df-rab 
 |-  { y e. A | ps } = { y | ( y e. A /\ ps ) }
15 12 13 14 3eqtr4i 
 |-  { x e. A | ph } = { y e. A | ps }