![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfun | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Ref | Expression |
---|---|
nfun.1 | ⊢ Ⅎ𝑥𝐴 |
nfun.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfun | ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-un 3945 | . 2 ⊢ (𝐴 ∪ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} | |
2 | nfun.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2882 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfun.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfcri 2882 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
6 | 3, 5 | nfor 1899 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵) |
7 | 6 | nfab 2901 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} |
8 | 1, 7 | nfcxfr 2893 | 1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 844 ∈ wcel 2098 {cab 2701 Ⅎwnfc 2875 ∪ cun 3938 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-un 3945 |
This theorem is referenced by: nfsymdif 4238 csbun 4430 iunxdif3 5088 nfsuc 6426 nfsup 9441 nfdju 9897 iunconn 23242 nosupbnd2 27553 noinfbnd2 27568 ordtconnlem1 33359 esumsplit 33506 measvuni 33667 bnj958 34406 bnj1000 34407 bnj1408 34502 bnj1446 34511 bnj1447 34512 bnj1448 34513 bnj1466 34519 bnj1467 34520 rdgssun 36715 exrecfnlem 36716 poimirlem16 36960 poimirlem19 36963 pimxrneun 44650 pimrecltpos 45875 |
Copyright terms: Public domain | W3C validator |