Theorem uniprg 4922

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 4923 to prove it from uniprg 4922. (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 3483	. . . . . . . . 9 ⊢ 𝑦 ∈ V
2	1	elpr 4649	. . . . . . . 8 ⊢ (𝑦 ∈ {𝐴, 𝐵} ↔ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵))
3	2	anbi2i 623	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)))
4		ancom 460	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ∧ 𝑥 ∈ 𝑦))
5		andir 1010	. . . . . . . 8 ⊢ (((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ∧ 𝑥 ∈ 𝑦) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
6	4, 5	bitri 275	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
7	3, 6	bitri 275	. . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
8	7	exbii 1847	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
9		19.43 1881	. . . . 5 ⊢ (∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
10	8, 9	bitri 275	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
11		clel3g 3660	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)))
12	11	bicomd 223	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
13	12	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
14		clel3g 3660	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
15	14	bicomd 223	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → (∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐵))
16	15	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐵))
17	13, 16	orbi12d 918	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
18	10, 17	bitrid 283	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
19	18	abbidv 2807	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)})
20		df-uni 4907	. 2 ⊢ ∪ {𝐴, 𝐵} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})}
21		df-un 3955	. 2 ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
22	19, 20, 21	3eqtr4g 2801	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2713   ∪ cun 3948  {cpr 4627  ∪ cuni 4906

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  df-sn 4626  df-pr 4628  df-uni 4907

This theorem is referenced by:  unipr  4923  unisng  4924  unexg  7764  wunun  10751  tskun  10827  gruun  10847  mrcun  17666  unopn  22910  indistopon  23009  unconn  23438  limcun  25931  sshjval3  31374  prsiga  34133  unelsiga  34136  unelldsys  34160  measxun2  34212  measssd  34217  carsgsigalem  34318  carsgclctun  34324  pmeasmono  34327  probun  34422  indispconn  35240  bj-prmoore  37117  kelac2  43082  onsucunipr  43390  onsucunitp  43391  oaun2  43399  oaun3  43400  mnuund  44302  fourierdlem70  46196  fourierdlem71  46197  saluncl  46337  prsal  46338  meadjun  46482  omeunle  46536  toplatjoin  48906