New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > unex | GIF version |
Description: The union of two sets is a set. (Contributed by SF, 12-Jan-2015.) |
Ref | Expression |
---|---|
boolex.1 | ⊢ A ∈ V |
boolex.2 | ⊢ B ∈ V |
Ref | Expression |
---|---|
unex | ⊢ (A ∪ B) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | boolex.1 | . 2 ⊢ A ∈ V | |
2 | boolex.2 | . 2 ⊢ B ∈ V | |
3 | unexg 4101 | . 2 ⊢ ((A ∈ V ∧ B ∈ V) → (A ∪ B) ∈ V) | |
4 | 1, 2, 3 | mp2an 653 | 1 ⊢ (A ∪ B) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1710 Vcvv 2859 ∪ cun 3207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-nin 3211 df-compl 3212 df-un 3214 |
This theorem is referenced by: vvex 4109 prex 4112 addcexlem 4382 eladdc 4398 nnc0suc 4412 addcass 4415 nncaddccl 4419 nnsucelrlem1 4424 nndisjeq 4429 preaddccan2lem1 4454 ltfinex 4464 ltfintrilem1 4465 tfinrelkex 4487 evenfinex 4503 oddfinex 4504 evenoddnnnul 4514 evenodddisjlem1 4515 nnadjoinlem1 4519 nnadjoin 4520 nnadjoinpw 4521 sfindbl 4530 vfinspss 4551 phiexg 4571 opexg 4587 proj1exg 4591 proj2exg 4592 proj2op 4601 phialllem2 4617 setconslem5 4735 1stex 4739 swapex 4742 fncup 5813 cupex 5816 clos1basesuc 5882 connexex 5913 unen 6048 enprmaplem4 6079 ncaddccl 6144 ce0addcnnul 6179 leconnnc 6218 addcdi 6250 nncdiv3lem2 6276 nchoicelem6 6294 nchoicelem16 6304 nchoicelem18 6306 frecxp 6314 |
Copyright terms: Public domain | W3C validator |