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 ⊢ Ⅎ _ x A
Assertion rabtru ⊢ x ∈ A | ⊤ = A

Proof

Step Hyp Ref Expression
1 rabtru.1 ⊢ Ⅎ _ x A
2 tru ⊢ ⊤
3 nfcv ⊢ Ⅎ _ x y
4 nftru ⊢ Ⅎ x ⊤
5 biidd ⊢ x = y → ⊤ ↔ ⊤
6 3 1 4 5 elrabf ⊢ y ∈ x ∈ A | ⊤ ↔ y ∈ A ∧ ⊤
7 2 6 mpbiran2 ⊢ y ∈ x ∈ A | ⊤ ↔ y ∈ A
8 7 eqriv ⊢ x ∈ A | ⊤ = A