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

Metamath Proof Explorer

Theorem elab2gw

Description: Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on x and A , which is not usually significant since B is usually a constant. (Contributed by SN, 16-May-2024)

Ref Expression
Hypotheses elabgw.1 
|- ( x = y -> ( ph <-> ps ) )
elabgw.2 
|- ( y = A -> ( ps <-> ch ) )
elab2gw.3 
|- B = { x | ph }
Assertion elab2gw 
|- ( A e. V -> ( A e. B <-> ch ) )

Proof

Step Hyp Ref Expression
1 elabgw.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 elabgw.2 
 |-  ( y = A -> ( ps <-> ch ) )
3 elab2gw.3 
 |-  B = { x | ph }
4 3 eleq2i 
 |-  ( A e. B <-> A e. { x | ph } )
5 1 2 elabgw 
 |-  ( A e. V -> ( A e. { x | ph } <-> ch ) )
6 4 5 bitrid 
 |-  ( A e. V -> ( A e. B <-> ch ) )