![]() |
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.) |
Ref | Expression |
---|---|
nfiun.1 | ⊢ Ⅎ𝑦𝐴 |
nfiun.2 | ⊢ Ⅎ𝑦𝐵 |
Ref | Expression |
---|---|
nfiun | ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iun 4554 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
2 | nfiun.1 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
3 | nfiun.2 | . . . . 5 ⊢ Ⅎ𝑦𝐵 | |
4 | 3 | nfcri 2787 | . . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵 |
5 | 2, 4 | nfrex 3036 | . . 3 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 |
6 | 5 | nfab 2798 | . 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} |
7 | 1, 6 | nfcxfr 2791 | 1 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 {cab 2637 Ⅎwnfc 2780 ∃wrex 2942 ∪ ciun 4552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-iun 4554 |
This theorem is referenced by: iunab 4598 disjxiun 4681 disjxiunOLD 4682 ovoliunnul 23321 iundisjf 29528 iundisj2f 29529 iundisjfi 29683 iundisj2fi 29684 bnj1498 31255 trpredlem1 31851 trpredrec 31862 ss2iundf 38268 fnlimcnv 40217 fnlimfvre 40224 fnlimabslt 40229 smfaddlem1 41292 smflimlem6 41305 smflim 41306 smfmullem4 41322 smflim2 41333 smflimsup 41355 smfliminf 41358 |
Copyright terms: Public domain | W3C validator |