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

Metamath Proof Explorer

Theorem elabd2

Description: Membership in a class abstraction, using implicit substitution. Deduction version of elab . (Contributed by GG, 12-Oct-2024) (Revised by BJ, 16-Oct-2024)

Ref Expression
Hypotheses elabd2.ex 
|- ( ph -> A e. V )
elabd2.eq 
|- ( ph -> B = { x | ps } )
elabd2.is 
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
Assertion elabd2 
|- ( ph -> ( A e. B <-> ch ) )

Proof

Step Hyp Ref Expression
1 elabd2.ex 
 |-  ( ph -> A e. V )
2 elabd2.eq 
 |-  ( ph -> B = { x | ps } )
3 elabd2.is 
 |-  ( ( ph /\ x = A ) -> ( ps <-> ch ) )
4 2 eleq2d 
 |-  ( ph -> ( A e. B <-> A e. { x | ps } ) )
5 elab6g 
 |-  ( A e. V -> ( A e. { x | ps } <-> A. x ( x = A -> ps ) ) )
6 4 5 sylan9bb 
 |-  ( ( ph /\ A e. V ) -> ( A e. B <-> A. x ( x = A -> ps ) ) )
7 elisset 
 |-  ( A e. V -> E. x x = A )
8 3 pm5.74da 
 |-  ( ph -> ( ( x = A -> ps ) <-> ( x = A -> ch ) ) )
9 8 albidv 
 |-  ( ph -> ( A. x ( x = A -> ps ) <-> A. x ( x = A -> ch ) ) )
10 19.23v 
 |-  ( A. x ( x = A -> ch ) <-> ( E. x x = A -> ch ) )
11 9 10 bitrdi 
 |-  ( ph -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ch ) ) )
12 pm5.5 
 |-  ( E. x x = A -> ( ( E. x x = A -> ch ) <-> ch ) )
13 11 12 sylan9bb 
 |-  ( ( ph /\ E. x x = A ) -> ( A. x ( x = A -> ps ) <-> ch ) )
14 7 13 sylan2 
 |-  ( ( ph /\ A e. V ) -> ( A. x ( x = A -> ps ) <-> ch ) )
15 6 14 bitrd 
 |-  ( ( ph /\ A e. V ) -> ( A e. B <-> ch ) )
16 1 15 mpdan 
 |-  ( ph -> ( A e. B <-> ch ) )