Theorem unab 4263

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 2343	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
2		df-clab 2744	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ (𝜑 ∨ 𝜓)} ↔ [𝑦 / 𝑥](𝜑 ∨ 𝜓))
3		df-clab 2744	. . . 4 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
4		df-clab 2744	. . . 4 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
5	3, 4	orbi12i 927	. . 3 ⊢ ((𝑦 ∈ {𝑥 ∣ 𝜑} ∨ 𝑦 ∈ {𝑥 ∣ 𝜓}) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
6	1, 2, 5	3bitr4ri 307	. 2 ⊢ ((𝑦 ∈ {𝑥 ∣ 𝜑} ∨ 𝑦 ∈ {𝑥 ∣ 𝜓}) ↔ 𝑦 ∈ {𝑥 ∣ (𝜑 ∨ 𝜓)})
7	6	uneqri 4112	1 ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)}

Syntax hints:   ∨ wo 860   = wceq 1563  [wsb 2093   ∈ wcel 2145  {cab 2743   ∪ cun 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912

This theorem is referenced by:  unrab  4270  rabun2  4279  hashf1lem2  14481  vdwlem6  17034  addsasslem1  28150  addsasslem2  28151  addsdilem1  28298  addsdilem2  28299  mulsasslem1  28310  mulsasslem2  28311  vtxdun  29736  satfvsuclem1  35717  satf0suclem  35733  fmlasuc0  35742  ecun  38899  sticksstones22  42792  diophun  43361