![]() |
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 4919 | . 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥∪ 𝐴) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ Ⅎ𝑥∪ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2876 ∪ cuni 4913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ral 3052 df-rex 3061 df-uni 4914 |
This theorem is referenced by: nfiota1 6508 nffrecs 8298 nfwrecsOLD 8332 nfsup 9494 ptunimpt 23590 disjabrex 32502 disjabrexf 32503 fnpreimac 32588 nfesum1 33873 nfesum2 33874 bnj1398 34879 bnj1446 34890 bnj1447 34891 bnj1448 34892 bnj1466 34898 bnj1467 34899 bnj1519 34910 bnj1520 34911 bnj1525 34914 bnj1523 34916 dfon2lem3 35609 mptsnunlem 37045 ptrest 37320 heibor1 37511 nfunidALT2 38667 nfunidALT 38668 disjinfi 44799 stoweidlem28 45649 stoweidlem59 45680 fourierdlem80 45807 saliinclf 45947 smfresal 46409 smfpimbor1lem2 46420 nfafv2 46831 nfsetrecs 48432 |
Copyright terms: Public domain | W3C validator |