|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > iuneq12d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) Remove DV conditions (Revised by GG, 1-Sep-2025.) | 
| Ref | Expression | 
|---|---|
| iuneq12d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) | 
| iuneq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) | 
| Ref | Expression | 
|---|---|
| iuneq12d | ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | iuneq12d.1 | . . . . . . 7 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | 1 | eleq2d 2826 | . . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | 
| 3 | 2 | anbi1d 631 | . . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑡 ∈ 𝐶))) | 
| 4 | 3 | rexbidv2 3174 | . . . 4 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶)) | 
| 5 | 4 | abbidv 2807 | . . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶} = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶}) | 
| 6 | df-iun 4992 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐴 𝑡 ∈ 𝐶} | |
| 7 | df-iun 4992 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑡 ∣ ∃𝑥 ∈ 𝐵 𝑡 ∈ 𝐶} | |
| 8 | 5, 6, 7 | 3eqtr4g 2801 | . 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | 
| 9 | iuneq12d.2 | . . . 4 ⊢ (𝜑 → 𝐶 = 𝐷) | |
| 10 | 9 | adantr 480 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷) | 
| 11 | 10 | iuneq2dv 5015 | . 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | 
| 12 | 8, 11 | eqtrd 2776 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 {cab 2713 ∃wrex 3069 ∪ ciun 4990 | 
| 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-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-rex 3070 df-v 3481 df-ss 3967 df-iun 4992 | 
| This theorem is referenced by: disjiunb 5132 cfsmolem 10311 cfsmo 10312 wunex2 10779 wuncval2 10788 imasval 17557 lpival 21335 cnextval 24070 cnextfval 24071 dvfval 25933 fedgmullem1 33681 irngval 33736 mblfinlem2 37666 heiborlem10 37828 iunrelexpmin1 43726 iunrelexpmin2 43730 colleq12d 44277 | 
| Copyright terms: Public domain | W3C validator |