![]() |
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 2821 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | orbi1d 915 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
3 | elun 4144 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶)) | |
4 | elun 4144 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 313 | . 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶))) |
6 | 5 | eqrdv 2729 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ∪ cun 3942 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-un 3949 |
This theorem is referenced by: uneq2 4153 uneq12 4154 uneq1i 4155 uneq1d 4158 unineq 4273 prprc1 4762 uniprgOLD 4921 relresfld 6264 unexb 7718 oarec 8545 xpider 8765 ralxpmap 8873 undifixp 8911 findcard2 9147 pwfilem 9160 unxpdom 9236 enp1ilem 9261 findcard2OLD 9267 domunfican 9303 pwfilemOLD 9329 fin1a2lem10 10386 incexclem 15764 lcmfunsnlem 16560 ramub1lem1 16941 ramub1 16943 mreexexlem3d 17572 mreexexlem4d 17573 ipodrsima 18476 mplsubglem 21487 mretopd 22525 iscldtop 22528 nconnsubb 22856 plyval 25636 spanun 30661 difeq 31620 unelldsys 32987 isros 32997 unelros 33000 difelros 33001 rossros 33009 measun 33040 inelcarsg 33141 actfunsnf1o 33447 actfunsnrndisj 33448 mrsubvrs 34344 altopthsn 34763 rankung 34968 bj-adjg1 35728 poimirlem28 36320 islshp 37654 lshpset2N 37794 paddval 38474 nacsfix 41221 eldioph4b 41320 eldioph4i 41321 diophren 41322 clsk3nimkb 42562 isotone1 42570 fiiuncl 43523 founiiun0 43659 infxrpnf 43929 meadjun 44951 hoidmvle 45089 |
Copyright terms: Public domain | W3C validator |