![]() |
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.) Avoid ax-11 2147, ax-12 2167. (Revised by SN, 14-May-2025.) |
Ref | Expression |
---|---|
nfiu1 | ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliun 5000 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
2 | nfre1 3279 | . . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 | |
3 | 1, 2 | nfxfr 1848 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 |
4 | 3 | nfci 2882 | 1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Ⅎwnfc 2879 ∃wrex 3067 ∪ ciun 4996 |
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-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-rex 3068 df-v 3473 df-iun 4998 |
This theorem is referenced by: ssiun2s 5051 disjxiun 5145 triun 5280 iunopeqop 5523 eliunxp 5840 opeliunxp2 5841 opeliunxp2f 8216 ixpf 8939 ixpiunwdom 9614 r1val1 9810 rankuni2b 9877 rankval4 9891 cplem2 9914 ac6num 10503 iunfo 10563 iundom2g 10564 inar1 10799 tskuni 10807 gsum2d2lem 19928 gsum2d2 19929 gsumcom2 19930 iunconn 23345 ptclsg 23532 cnextfvval 23982 ssiun2sf 32363 djussxp2 32447 2ndresdju 32448 aciunf1lem 32461 fsumiunle 32605 irngnzply1 33369 esum2dlem 33711 esum2d 33712 esumiun 33713 sigapildsys 33781 bnj958 34571 bnj1000 34572 bnj981 34581 bnj1398 34665 bnj1408 34667 ralssiun 36886 iunconnlem2 44374 iunmapss 44588 iunmapsn 44590 allbutfi 44775 fsumiunss 44963 dvnprodlem1 45334 dvnprodlem2 45335 sge0iunmptlemfi 45801 sge0iunmptlemre 45803 sge0iunmpt 45806 iundjiun 45848 voliunsge0lem 45860 caratheodorylem2 45915 smflimmpt 46198 smflimsuplem7 46214 eliunxp2 47397 |
Copyright terms: Public domain | W3C validator |