![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfiun | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2365. See nfiung 5029 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) |
Ref | Expression |
---|---|
nfiun.1 | ⊢ Ⅎ𝑦𝐴 |
nfiun.2 | ⊢ Ⅎ𝑦𝐵 |
Ref | Expression |
---|---|
nfiun | ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iun 4999 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
2 | nfiun.1 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
3 | nfiun.2 | . . . . 5 ⊢ Ⅎ𝑦𝐵 | |
4 | 3 | nfcri 2882 | . . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵 |
5 | 2, 4 | nfrexw 3300 | . . 3 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 |
6 | 5 | nfab 2897 | . 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} |
7 | 1, 6 | nfcxfr 2889 | 1 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 {cab 2702 Ⅎwnfc 2875 ∃wrex 3059 ∪ ciun 4997 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rex 3060 df-iun 4999 |
This theorem is referenced by: iunab 5055 disjxiun 5146 ttrclselem1 9750 ttrclselem2 9751 ovoliunnul 25480 iundisjf 32458 iundisj2f 32459 iundisjfi 32646 iundisj2fi 32647 bnj1498 34820 ss2iundf 43228 nfcoll 43832 fnlimcnv 45190 fnlimfvre 45197 fnlimabslt 45202 smfaddlem1 46286 smflimlem6 46299 smflim 46300 smfmullem4 46317 smflim2 46329 smflimsup 46351 smfliminf 46354 fsupdm 46365 finfdm 46369 |
Copyright terms: Public domain | W3C validator |