Metamath Proof Explorer

Theorem bj-rabtrALT

Description: Alternate proof of bj-rabtr . (Contributed by BJ, 22-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-rabtrALT 
|- { x e. A | T. } = A

Proof

Step Hyp Ref Expression
1 nfrab1 
 |-  F/_ x { x e. A | T. }
2 nfcv 
 |-  F/_ x A
3 1 2 cleqf 
 |-  ( { x e. A | T. } = A <-> A. x ( x e. { x e. A | T. } <-> x e. A ) )
4 tru 
 |-  T.
5 rabid 
 |-  ( x e. { x e. A | T. } <-> ( x e. A /\ T. ) )
6 4 5 mpbiran2 
 |-  ( x e. { x e. A | T. } <-> x e. A )
7 3 6 mpgbir 
 |-  { x e. A | T. } = A