![]() |
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 | dfuni2 4708 | . 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧} | |
2 | nfuni.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfv 1873 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑧 | |
4 | 2, 3 | nfrex 3247 | . . 3 ⊢ Ⅎ𝑥∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 |
5 | 4 | nfab 2932 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧} |
6 | 1, 5 | nfcxfr 2924 | 1 ⊢ Ⅎ𝑥∪ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: {cab 2753 Ⅎwnfc 2910 ∃wrex 3083 ∪ cuni 4706 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-uni 4707 |
This theorem is referenced by: nfiota1 6148 nfwrecs 7745 nfsup 8702 ptunimpt 21897 disjabrex 30088 disjabrexf 30089 fnpreimac 30168 nfesum1 30900 nfesum2 30901 bnj1398 31912 bnj1446 31923 bnj1447 31924 bnj1448 31925 bnj1466 31931 bnj1467 31932 bnj1519 31943 bnj1520 31944 bnj1525 31947 bnj1523 31949 dfon2lem3 32490 nffrecs 32581 mptsnunlem 33996 ptrest 34280 heibor1 34478 nfunidALT2 35498 nfunidALT 35499 disjinfi 40824 stoweidlem28 41690 stoweidlem59 41721 fourierdlem80 41848 smfresal 42440 smfpimbor1lem2 42451 nfafv2 42769 nfsetrecs 44096 |
Copyright terms: Public domain | W3C validator |