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

Theorem unab 4308
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 2307 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
2 df-clab 2715 . . 3 (𝑦 ∈ {𝑥 ∣ (𝜑𝜓)} ↔ [𝑦 / 𝑥](𝜑𝜓))
3 df-clab 2715 . . . 4 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
4 df-clab 2715 . . . 4 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
53, 4orbi12i 915 . . 3 ((𝑦 ∈ {𝑥𝜑} ∨ 𝑦 ∈ {𝑥𝜓}) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
61, 2, 53bitr4ri 304 . 2 ((𝑦 ∈ {𝑥𝜑} ∨ 𝑦 ∈ {𝑥𝜓}) ↔ 𝑦 ∈ {𝑥 ∣ (𝜑𝜓)})
76uneqri 4156 1 ({𝑥𝜑} ∪ {𝑥𝜓}) = {𝑥 ∣ (𝜑𝜓)}
Colors of variables: wff setvar class
Syntax hints:  wo 848   = wceq 1540  [wsb 2064  wcel 2108  {cab 2714  cun 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956
This theorem is referenced by:  unrab  4315  rabun2  4324  dmun  5921  hashf1lem2  14495  vdwlem6  17024  addsasslem1  28036  addsasslem2  28037  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  vtxdun  29499  satfvsuclem1  35364  satf0suclem  35380  fmlasuc0  35389  sticksstones22  42169  diophun  42784
  Copyright terms: Public domain W3C validator