Theorem uniprg 4925

Description: The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.) Avoid using unipr 4926 to prove it from uniprg 4925. (Revised by BJ, 1-Sep-2024.)

Assertion

Ref	Expression
uniprg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))

Proof of Theorem uniprg

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3465	. . . . . . . . 9 ⊢ 𝑦 ∈ V
2	1	elpr 4654	. . . . . . . 8 ⊢ (𝑦 ∈ {𝐴, 𝐵} ↔ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵))
3	2	anbi2i 621	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)))
4		ancom 459	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ∧ 𝑥 ∈ 𝑦))
5		andir 1006	. . . . . . . 8 ⊢ (((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ∧ 𝑥 ∈ 𝑦) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
6	4, 5	bitri 274	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
7	3, 6	bitri 274	. . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
8	7	exbii 1842	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
9		19.43 1877	. . . . 5 ⊢ (∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
10	8, 9	bitri 274	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
11		clel3g 3645	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)))
12	11	bicomd 222	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
13	12	adantr 479	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
14		clel3g 3645	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
15	14	bicomd 222	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → (∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐵))
16	15	adantl 480	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐵))
17	13, 16	orbi12d 916	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
18	10, 17	bitrid 282	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
19	18	abbidv 2794	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)})
20		df-uni 4910	. 2 ⊢ ∪ {𝐴, 𝐵} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})}
21		df-un 3949	. 2 ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
22	19, 20, 21	3eqtr4g 2790	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1533  ∃wex 1773   ∈ wcel 2098  {cab 2702   ∪ cun 3942  {cpr 4632  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3949  df-sn 4631  df-pr 4633  df-uni 4910

This theorem is referenced by:  unipr  4926  unisng  4929  wunun  10735  tskun  10811  gruun  10831  mrcun  17605  unopn  22849  indistopon  22948  unconn  23377  limcun  25868  sshjval3  31236  prsiga  33878  unelsiga  33881  unelldsys  33905  measxun2  33957  measssd  33962  carsgsigalem  34063  carsgclctun  34069  pmeasmono  34072  probun  34167  indispconn  34972  bj-prmoore  36722  kelac2  42628  onsucunipr  42940  onsucunitp  42941  oaun2  42949  oaun3  42950  mnuund  43854  fourierdlem70  45699  fourierdlem71  45700  saluncl  45840  prsal  45841  meadjun  45985  omeunle  46039  toplatjoin  48196