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 4837 | . 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥∪ 𝐴) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ Ⅎ𝑥∪ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2961 ∪ cuni 4831 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-uni 4832 |
This theorem is referenced by: nfiota1 6310 nfwrecs 7943 nfsup 8909 ptunimpt 22197 disjabrex 30326 disjabrexf 30327 fnpreimac 30410 nfesum1 31294 nfesum2 31295 bnj1398 32301 bnj1446 32312 bnj1447 32313 bnj1448 32314 bnj1466 32320 bnj1467 32321 bnj1519 32332 bnj1520 32333 bnj1525 32336 bnj1523 32338 dfon2lem3 33025 nffrecs 33115 mptsnunlem 34613 ptrest 34885 heibor1 35082 nfunidALT2 36099 nfunidALT 36100 disjinfi 41447 stoweidlem28 42307 stoweidlem59 42338 fourierdlem80 42465 smfresal 43057 smfpimbor1lem2 43068 nfafv2 43411 nfsetrecs 44783 |
Copyright terms: Public domain | W3C validator |