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

Metamath Proof Explorer

Theorem rabtru

Description: Abstract builder using the constant wff T. . (Contributed by Thierry Arnoux, 4-May-2020)

Ref Expression
Hypothesis rabtru.1 ⊢ Ⅎ 𝑥 𝐴
Assertion rabtru { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴

Proof

Step Hyp Ref Expression
1 rabtru.1 ⊢ Ⅎ 𝑥 𝐴
2 tru ⊢ ⊤
3 nfcv ⊢ Ⅎ 𝑥 𝑦
4 nftru ⊢ Ⅎ 𝑥 ⊤
5 biidd ⊢ ( 𝑥 = 𝑦 → ( ⊤ ↔ ⊤ ) )
6 3 1 4 5 elrabf ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ⊤ } ↔ ( 𝑦 ∈ 𝐴 ∧ ⊤ ) )
7 2 6 mpbiran2 ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ⊤ } ↔ 𝑦 ∈ 𝐴 )
8 7 eqriv ⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴