![]() |
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 3868 | . 2 ⊢ (𝐴 ∪ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} | |
2 | nfun.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2943 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfun.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfcri 2943 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
6 | 3, 5 | nfor 1886 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵) |
7 | 6 | nfab 2955 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} |
8 | 1, 7 | nfcxfr 2947 | 1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 842 ∈ wcel 2081 {cab 2775 Ⅎwnfc 2933 ∪ cun 3861 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-un 3868 |
This theorem is referenced by: nfsymdif 4147 csbun 4309 iunxdif3 4920 nfsuc 6142 nfsup 8766 nfdju 9187 iunconn 21725 ordtconnlem1 30789 esumsplit 30934 measvuni 31095 bnj958 31833 bnj1000 31834 bnj1408 31927 bnj1446 31936 bnj1447 31937 bnj1448 31938 bnj1466 31944 bnj1467 31945 nosupbnd2 32831 rdgssun 34215 exrecfnlem 34216 poimirlem16 34464 poimirlem19 34467 pimrecltpos 42555 |
Copyright terms: Public domain | W3C validator |