Theorem rabtru 3551

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

Hypothesis

Ref	Expression
rabtru.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
rabtru	⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴

Proof of Theorem rabtru

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcv 2939	. . . 4 ⊢ Ⅎ𝑥𝑦
2		rabtru.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nftru 1900	. . . 4 ⊢ Ⅎ𝑥⊤
4		biidd 254	. . . 4 ⊢ (𝑥 = 𝑦 → (⊤ ↔ ⊤))
5	1, 2, 3, 4	elrabf 3550	. . 3 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ⊤} ↔ (𝑦 ∈ 𝐴 ∧ ⊤))
6		tru 1658	. . . 4 ⊢ ⊤
7	6	biantru 526	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ 𝐴 ∧ ⊤))
8	5, 7	bitr4i 270	. 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ⊤} ↔ 𝑦 ∈ 𝐴)
9	8	eqriv 2794	1 ⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴

Syntax hints:   ∧ wa 385   = wceq 1653  ⊤wtru 1654   ∈ wcel 2157  Ⅎwnfc 2926  {crab 3091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-rab 3096  df-v 3385

This theorem is referenced by:  mptexgf  6712  aciunf1  29974