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 2822 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | orbi1d 916 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
3 | elun 4049 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶)) | |
4 | elun 4049 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 317 | . 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶))) |
6 | 5 | eqrdv 2737 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 = wceq 1542 ∈ wcel 2114 ∪ cun 3851 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3402 df-un 3858 |
This theorem is referenced by: uneq2 4057 uneq12 4058 uneq1i 4059 uneq1d 4062 unineq 4178 prprc1 4666 uniprgOLD 4826 relresfld 6118 unexb 7502 oarec 8232 xpider 8412 ralxpmap 8519 undifixp 8557 findcard2 8776 pwfilem 8788 unxpdom 8817 enp1ilem 8842 findcard2OLD 8847 domunfican 8878 pwfilemOLD 8904 fin1a2lem10 9922 incexclem 15297 lcmfunsnlem 16095 ramub1lem1 16475 ramub1 16477 mreexexlem3d 17033 mreexexlem4d 17034 ipodrsima 17904 mplsubglem 20828 mretopd 21856 iscldtop 21859 nconnsubb 22187 plyval 24955 spanun 29493 difeq 30452 unelldsys 31709 isros 31719 unelros 31722 difelros 31723 rossros 31731 measun 31762 inelcarsg 31861 actfunsnf1o 32167 actfunsnrndisj 32168 mrsubvrs 33068 altopthsn 33919 rankung 34124 poimirlem28 35461 islshp 36649 lshpset2N 36789 paddval 37468 nacsfix 40147 eldioph4b 40246 eldioph4i 40247 diophren 40248 clsk3nimkb 41237 isotone1 41245 fiiuncl 42192 founiiun0 42307 infxrpnf 42566 meadjun 43583 hoidmvle 43721 |
Copyright terms: Public domain | W3C validator |