|   | 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 2829 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
| 2 | 1 | orbi1d 916 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) | 
| 3 | elun 4152 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶)) | |
| 4 | elun 4152 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | . 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶))) | 
| 6 | 5 | eqrdv 2734 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∨ wo 847 = wceq 1539 ∈ wcel 2107 ∪ cun 3948 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-un 3955 | 
| This theorem is referenced by: uneq2 4161 uneq12 4162 uneq1i 4163 uneq1d 4166 unineq 4287 prprc1 4764 relresfld 6295 unexbOLD 7769 oarec 8601 xpider 8829 ralxpmap 8937 undifixp 8975 findcard2 9205 unxpdom 9290 enp1ilem 9313 pwfilem 9357 domunfican 9362 fin1a2lem10 10450 incexclem 15873 lcmfunsnlem 16679 ramub1lem1 17065 ramub1 17067 mreexexlem3d 17690 mreexexlem4d 17691 ipodrsima 18587 mplsubglem 22020 mretopd 23101 iscldtop 23104 nconnsubb 23432 plyval 26233 spanun 31565 difeq 32538 unelldsys 34160 isros 34170 unelros 34173 difelros 34174 rossros 34182 measun 34213 inelcarsg 34314 actfunsnf1o 34620 actfunsnrndisj 34621 mrsubvrs 35528 altopthsn 35963 rankung 36168 bj-adjg1 37045 poimirlem28 37656 islshp 38981 lshpset2N 39121 paddval 39801 nacsfix 42728 eldioph4b 42827 eldioph4i 42828 diophren 42829 clsk3nimkb 44058 isotone1 44066 fiiuncl 45075 founiiun0 45200 infxrpnf 45462 meadjun 46482 hoidmvle 46620 | 
| Copyright terms: Public domain | W3C validator |