| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > unab | Structured version Visualization version GIF version | ||
| Description: Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| Ref | Expression |
|---|---|
| unab | ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbor 2307 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓)) | |
| 2 | df-clab 2715 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ (𝜑 ∨ 𝜓)} ↔ [𝑦 / 𝑥](𝜑 ∨ 𝜓)) | |
| 3 | df-clab 2715 | . . . 4 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
| 4 | df-clab 2715 | . . . 4 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓) | |
| 5 | 3, 4 | orbi12i 915 | . . 3 ⊢ ((𝑦 ∈ {𝑥 ∣ 𝜑} ∨ 𝑦 ∈ {𝑥 ∣ 𝜓}) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓)) |
| 6 | 1, 2, 5 | 3bitr4ri 304 | . 2 ⊢ ((𝑦 ∈ {𝑥 ∣ 𝜑} ∨ 𝑦 ∈ {𝑥 ∣ 𝜓}) ↔ 𝑦 ∈ {𝑥 ∣ (𝜑 ∨ 𝜓)}) |
| 7 | 6 | uneqri 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 |