Metamath Proof Explorer

Theorem bj-denoteslem

Description: Lemma for bj-denotes . (Contributed by BJ, 24-Apr-2024) (Proof modification is discouraged.)

Ref Expression
Assertion bj-denoteslem 
|- ( E. x x = A <-> A e. { y | T. } )

Proof

Step Hyp Ref Expression
1 vextru 
 |-  x e. { y | T. }
2 1 biantru 
 |-  ( x = A <-> ( x = A /\ x e. { y | T. } ) )
3 2 exbii 
 |-  ( E. x x = A <-> E. x ( x = A /\ x e. { y | T. } ) )
4 dfclel 
 |-  ( A e. { y | T. } <-> E. x ( x = A /\ x e. { y | T. } ) )
5 3 4 bitr4i 
 |-  ( E. x x = A <-> A e. { y | T. } )