Theorem unab 4298

Description: Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
unab	⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)}

Proof of Theorem unab

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbor 2303	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
2		df-clab 2710	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ (𝜑 ∨ 𝜓)} ↔ [𝑦 / 𝑥](𝜑 ∨ 𝜓))
3		df-clab 2710	. . . 4 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
4		df-clab 2710	. . . 4 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
5	3, 4	orbi12i 913	. . 3 ⊢ ((𝑦 ∈ {𝑥 ∣ 𝜑} ∨ 𝑦 ∈ {𝑥 ∣ 𝜓}) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
6	1, 2, 5	3bitr4ri 303	. 2 ⊢ ((𝑦 ∈ {𝑥 ∣ 𝜑} ∨ 𝑦 ∈ {𝑥 ∣ 𝜓}) ↔ 𝑦 ∈ {𝑥 ∣ (𝜑 ∨ 𝜓)})
7	6	uneqri 4151	1 ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)}

Syntax hints:   ∨ wo 845   = wceq 1541  [wsb 2067   ∈ wcel 2106  {cab 2709   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953

This theorem is referenced by:  unrab  4305  rabun2  4313  dmun  5910  hashf1lem2  14419  vdwlem6  16921  addsasslem1  27496  addsasslem2  27497  addsdilem1  27616  addsdilem2  27617  mulsasslem1  27628  mulsasslem2  27629  vtxdun  28776  satfvsuclem1  34419  satf0suclem  34435  fmlasuc0  34444  sticksstones22  41076  diophun  41599