![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfiu1 | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) |
Ref | Expression |
---|---|
nfiu1 | ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iun 4788 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | |
2 | nfre1 3245 | . . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 | |
3 | 2 | nfab 2932 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
4 | 1, 3 | nfcxfr 2924 | 1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2048 {cab 2753 Ⅎwnfc 2910 ∃wrex 3083 ∪ ciun 4786 |
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-rex 3088 df-iun 4788 |
This theorem is referenced by: ssiun2s 4832 disjxiun 4920 triun 5037 iunopeqop 5260 eliunxp 5551 opeliunxp2 5552 opeliunxp2f 7672 ixpf 8273 ixpiunwdom 8842 r1val1 9001 rankuni2b 9068 rankval4 9082 cplem2 9105 ac6num 9691 iunfo 9751 iundom2g 9752 inar1 9987 tskuni 9995 gsum2d2lem 18836 gsum2d2 18837 gsumcom2 18838 iunconn 21730 ptclsg 21917 cnextfvval 22367 ssiun2sf 30070 aciunf1lem 30159 fsumiunle 30280 esum2dlem 30952 esum2d 30953 esumiun 30954 sigapildsys 31023 bnj958 31820 bnj1000 31821 bnj981 31830 bnj1398 31912 bnj1408 31914 ralssiun 34064 iunconnlem2 40632 iunmapss 40849 iunmapsn 40851 allbutfi 41041 fsumiunss 41233 dvnprodlem1 41607 dvnprodlem2 41608 sge0iunmptlemfi 42072 sge0iunmptlemre 42074 sge0iunmpt 42077 iundjiun 42119 voliunsge0lem 42131 caratheodorylem2 42186 smflimmpt 42461 smflimsuplem7 42477 eliunxp2 43686 |
Copyright terms: Public domain | W3C validator |