![]() |
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 4870 | . 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥∪ 𝐴) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ Ⅎ𝑥∪ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2886 ∪ cuni 4864 |
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 2709 |
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 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ral 3064 df-rex 3073 df-uni 4865 |
This theorem is referenced by: nfiota1 6448 nffrecs 8207 nfwrecsOLD 8241 nfsup 9346 ptunimpt 22898 disjabrex 31328 disjabrexf 31329 fnpreimac 31415 nfesum1 32443 nfesum2 32444 bnj1398 33450 bnj1446 33461 bnj1447 33462 bnj1448 33463 bnj1466 33469 bnj1467 33470 bnj1519 33481 bnj1520 33482 bnj1525 33485 bnj1523 33487 dfon2lem3 34170 mptsnunlem 35741 ptrest 36009 heibor1 36201 nfunidALT2 37363 nfunidALT 37364 disjinfi 43311 stoweidlem28 44164 stoweidlem59 44195 fourierdlem80 44322 saliinclf 44462 smfresal 44924 smfpimbor1lem2 44935 nfafv2 45345 nfsetrecs 47026 |
Copyright terms: Public domain | W3C validator |