Theorem 3unrab 32651

Description: Union of three restricted class abstractions. (Contributed by Thierry Arnoux, 6-Jul-2025.)

Assertion

Ref	Expression
3unrab	⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) ∪ {𝑥 ∈ 𝐴 ∣ 𝜒}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓 ∨ 𝜒)}

Proof of Theorem 3unrab

Step	Hyp	Ref	Expression
1		unrab 4267	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} ∪ {𝑥 ∈ 𝐴 ∣ 𝜒}) = {𝑥 ∈ 𝐴 ∣ ((𝜑 ∨ 𝜓) ∨ 𝜒)}
2		unrab 4267	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}
3	2	uneq1i 4117	. 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) ∪ {𝑥 ∈ 𝐴 ∣ 𝜒}) = ({𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} ∪ {𝑥 ∈ 𝐴 ∣ 𝜒})
4		df-3or 1098	. . 3 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
5	4	rabbii 3418	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓 ∨ 𝜒)} = {𝑥 ∈ 𝐴 ∣ ((𝜑 ∨ 𝜓) ∨ 𝜒)}
6	1, 3, 5	3eqtr4i 2794	1 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) ∪ {𝑥 ∈ 𝐴 ∣ 𝜒}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓 ∨ 𝜒)}

Syntax hints:   ∨ wo 858   ∨ w3o 1096   = wceq 1559  {crab 3413   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-tru 1562  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-un 3909

This theorem is referenced by:  constrfin  34004