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

Metamath Proof Explorer

Theorem elrab3t

Description: Membership in a restricted class abstraction, using implicit substitution. (Closed theorem version of elrab3 .) (Contributed by Thierry Arnoux, 31-Aug-2017)

Ref Expression
Assertion elrab3t 
|- ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A e. { x e. B | ph } <-> ps ) )

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. B | ph } = { x | ( x e. B /\ ph ) }
2 1 eleq2i 
 |-  ( A e. { x e. B | ph } <-> A e. { x | ( x e. B /\ ph ) } )
3 id 
 |-  ( A e. B -> A e. B )
4 nfa1 
 |-  F/ x A. x ( x = A -> ( ph <-> ps ) )
5 nfv 
 |-  F/ x A e. B
6 4 5 nfan 
 |-  F/ x ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B )
7 sp 
 |-  ( A. x ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ph <-> ps ) ) )
8 eleq1 
 |-  ( x = A -> ( x e. B <-> A e. B ) )
9 8 biimparc 
 |-  ( ( A e. B /\ x = A ) -> x e. B )
10 9 biantrurd 
 |-  ( ( A e. B /\ x = A ) -> ( ph <-> ( x e. B /\ ph ) ) )
11 10 bibi1d 
 |-  ( ( A e. B /\ x = A ) -> ( ( ph <-> ps ) <-> ( ( x e. B /\ ph ) <-> ps ) ) )
12 11 pm5.74da 
 |-  ( A e. B -> ( ( x = A -> ( ph <-> ps ) ) <-> ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) ) )
13 7 12 syl5ibcom 
 |-  ( A. x ( x = A -> ( ph <-> ps ) ) -> ( A e. B -> ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) ) )
14 13 imp 
 |-  ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) )
15 6 14 alrimi 
 |-  ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> A. x ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) )
16 elabgt 
 |-  ( ( A e. B /\ A. x ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) ) -> ( A e. { x | ( x e. B /\ ph ) } <-> ps ) )
17 3 15 16 syl2an2 
 |-  ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A e. { x | ( x e. B /\ ph ) } <-> ps ) )
18 2 17 bitrid 
 |-  ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A e. { x e. B | ph } <-> ps ) )