MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unab Structured version   Visualization version   GIF version

Theorem unab 4314
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.
StepHypRef Expression
1 sbor 2306 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
2 df-clab 2713 . . 3 (𝑦 ∈ {𝑥 ∣ (𝜑𝜓)} ↔ [𝑦 / 𝑥](𝜑𝜓))
3 df-clab 2713 . . . 4 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
4 df-clab 2713 . . . 4 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
53, 4orbi12i 914 . . 3 ((𝑦 ∈ {𝑥𝜑} ∨ 𝑦 ∈ {𝑥𝜓}) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
61, 2, 53bitr4ri 304 . 2 ((𝑦 ∈ {𝑥𝜑} ∨ 𝑦 ∈ {𝑥𝜓}) ↔ 𝑦 ∈ {𝑥 ∣ (𝜑𝜓)})
76uneqri 4166 1 ({𝑥𝜑} ∪ {𝑥𝜓}) = {𝑥 ∣ (𝜑𝜓)}
Colors of variables: wff setvar class
Syntax hints:  wo 847   = wceq 1537  [wsb 2062  wcel 2106  {cab 2712  cun 3961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968
This theorem is referenced by:  unrab  4321  rabun2  4330  dmun  5924  hashf1lem2  14492  vdwlem6  17020  addsasslem1  28051  addsasslem2  28052  addsdilem1  28192  addsdilem2  28193  mulsasslem1  28204  mulsasslem2  28205  vtxdun  29514  satfvsuclem1  35344  satf0suclem  35360  fmlasuc0  35369  sticksstones22  42150  diophun  42761
  Copyright terms: Public domain W3C validator