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	⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ⊤ }
2		nfcv	⊢ Ⅎ 𝑥 𝐴
3	1 2	cleqf	⊢ ( { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ⊤ } ↔ 𝑥 ∈ 𝐴 ) )
4		tru	⊢ ⊤
5		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ⊤ } ↔ ( 𝑥 ∈ 𝐴 ∧ ⊤ ) )
6	4 5	mpbiran2	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ⊤ } ↔ 𝑥 ∈ 𝐴 )
7	3 6	mpgbir	⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴