Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uneq1 | Structured version Visualization version GIF version |
Description: Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.) |
Ref | Expression |
---|---|
uneq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2827 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | orbi1d 914 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
3 | elun 4083 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶)) | |
4 | elun 4083 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 314 | . 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶))) |
6 | 5 | eqrdv 2736 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 844 = wceq 1539 ∈ wcel 2106 ∪ cun 3885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-un 3892 |
This theorem is referenced by: uneq2 4091 uneq12 4092 uneq1i 4093 uneq1d 4096 unineq 4211 prprc1 4701 uniprgOLD 4859 relresfld 6179 unexb 7598 oarec 8393 xpider 8577 ralxpmap 8684 undifixp 8722 findcard2 8947 pwfilem 8960 unxpdom 9030 enp1ilem 9051 findcard2OLD 9056 domunfican 9087 pwfilemOLD 9113 fin1a2lem10 10165 incexclem 15548 lcmfunsnlem 16346 ramub1lem1 16727 ramub1 16729 mreexexlem3d 17355 mreexexlem4d 17356 ipodrsima 18259 mplsubglem 21205 mretopd 22243 iscldtop 22246 nconnsubb 22574 plyval 25354 spanun 29907 difeq 30865 unelldsys 32126 isros 32136 unelros 32139 difelros 32140 rossros 32148 measun 32179 inelcarsg 32278 actfunsnf1o 32584 actfunsnrndisj 32585 mrsubvrs 33484 altopthsn 34263 rankung 34468 poimirlem28 35805 islshp 36993 lshpset2N 37133 paddval 37812 nacsfix 40534 eldioph4b 40633 eldioph4i 40634 diophren 40635 clsk3nimkb 41650 isotone1 41658 fiiuncl 42613 founiiun0 42728 infxrpnf 42986 meadjun 44000 hoidmvle 44138 |
Copyright terms: Public domain | W3C validator |