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 2371. See nfiung 4910 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
Ref | Expression |
---|---|
nfiun.1 | ⊢ Ⅎ𝑦𝐴 |
nfiun.2 | ⊢ Ⅎ𝑦𝐵 |
Ref | Expression |
---|---|
nfiun | ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iun 4880 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
2 | nfiun.1 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
3 | nfiun.2 | . . . . 5 ⊢ Ⅎ𝑦𝐵 | |
4 | 3 | nfcri 2886 | . . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵 |
5 | 2, 4 | nfrex 3218 | . . 3 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 |
6 | 5 | nfab 2905 | . 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} |
7 | 1, 6 | nfcxfr 2897 | 1 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 {cab 2716 Ⅎwnfc 2879 ∃wrex 3054 ∪ ciun 4878 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-iun 4880 |
This theorem is referenced by: iunab 4934 disjxiun 5024 ovoliunnul 24252 iundisjf 30494 iundisj2f 30495 iundisjfi 30684 iundisj2fi 30685 bnj1498 32604 trpredlem1 33361 trpredrec 33372 ss2iundf 40797 nfcoll 41400 fnlimcnv 42734 fnlimfvre 42741 fnlimabslt 42746 smfaddlem1 43821 smflimlem6 43834 smflim 43835 smfmullem4 43851 smflim2 43862 smflimsup 43884 smfliminf 43887 |
Copyright terms: Public domain | W3C validator |