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

Metamath Proof Explorer

Theorem rabrabi

Description: Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022) Avoid ax-10 , ax-11 and ax-12 . (Revised by GG, 12-Oct-2024)

Ref Expression
Hypothesis rabrabi.1 
|- ( x = y -> ( ch <-> ph ) )
Assertion rabrabi 
|- { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) }

Proof

Step Hyp Ref Expression
1 rabrabi.1 
 |-  ( x = y -> ( ch <-> ph ) )
2 df-rab 
 |-  { y e. A | ph } = { y | ( y e. A /\ ph ) }
3 2 eleq2i 
 |-  ( x e. { y e. A | ph } <-> x e. { y | ( y e. A /\ ph ) } )
4 df-clab 
 |-  ( x e. { y | ( y e. A /\ ph ) } <-> [ x / y ] ( y e. A /\ ph ) )
5 eleq1w 
 |-  ( y = x -> ( y e. A <-> x e. A ) )
6 1 bicomd 
 |-  ( x = y -> ( ph <-> ch ) )
7 6 equcoms 
 |-  ( y = x -> ( ph <-> ch ) )
8 5 7 anbi12d 
 |-  ( y = x -> ( ( y e. A /\ ph ) <-> ( x e. A /\ ch ) ) )
9 8 sbievw 
 |-  ( [ x / y ] ( y e. A /\ ph ) <-> ( x e. A /\ ch ) )
10 3 4 9 3bitri 
 |-  ( x e. { y e. A | ph } <-> ( x e. A /\ ch ) )
11 10 anbi1i 
 |-  ( ( x e. { y e. A | ph } /\ ps ) <-> ( ( x e. A /\ ch ) /\ ps ) )
12 anass 
 |-  ( ( ( x e. A /\ ch ) /\ ps ) <-> ( x e. A /\ ( ch /\ ps ) ) )
13 11 12 bitri 
 |-  ( ( x e. { y e. A | ph } /\ ps ) <-> ( x e. A /\ ( ch /\ ps ) ) )
14 13 rabbia2 
 |-  { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) }