![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfuni | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
nfuni.1 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfuni | ⊢ Ⅎ𝑥∪ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfuni.1 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | id 22 | . . 3 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴) | |
3 | 2 | nfunid 4915 | . 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥∪ 𝐴) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ Ⅎ𝑥∪ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2884 ∪ cuni 4909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-uni 4910 |
This theorem is referenced by: nfiota1 6498 nffrecs 8268 nfwrecsOLD 8302 nfsup 9446 ptunimpt 23099 disjabrex 31813 disjabrexf 31814 fnpreimac 31896 nfesum1 33038 nfesum2 33039 bnj1398 34045 bnj1446 34056 bnj1447 34057 bnj1448 34058 bnj1466 34064 bnj1467 34065 bnj1519 34076 bnj1520 34077 bnj1525 34080 bnj1523 34082 dfon2lem3 34757 mptsnunlem 36219 ptrest 36487 heibor1 36678 nfunidALT2 37839 nfunidALT 37840 disjinfi 43891 stoweidlem28 44744 stoweidlem59 44775 fourierdlem80 44902 saliinclf 45042 smfresal 45504 smfpimbor1lem2 45515 nfafv2 45926 nfsetrecs 47731 |
Copyright terms: Public domain | W3C validator |