New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > uneq2i | GIF version |
Description: Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
uneq1i.1 | ⊢ A = B |
Ref | Expression |
---|---|
uneq2i | ⊢ (C ∪ A) = (C ∪ B) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1i.1 | . 2 ⊢ A = B | |
2 | uneq2 3412 | . 2 ⊢ (A = B → (C ∪ A) = (C ∪ B)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (C ∪ A) = (C ∪ B) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1642 ∪ 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 |
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: un4 3423 unundir 3425 difun2 3629 difdifdir 3637 dfif5 3674 qdass 3819 qdassr 3820 ssunpr 3868 iununi 4050 pw1eqadj 4332 nncaddccl 4419 ltfintrilem1 4465 ncfinraise 4481 tfinsuc 4498 nnadjoin 4520 sfindbl 4530 tfinnn 4534 fvsnun1 5447 sbthlem1 6203 leconnnc 6218 nchoicelem16 6304 |
Copyright terms: Public domain | W3C validator |