Theorem uniprg 4872

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 4873 to prove it from uniprg 4872. (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 3440	. . . . . . . . 9 ⊢ 𝑦 ∈ V
2	1	elpr 4598	. . . . . . . 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 1849	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
9		19.43 1883	. . . . 5 ⊢ (∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
10	8, 9	bitri 275	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
11		clel3g 3611	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)))
12	11	bicomd 223	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
13	12	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
14		clel3g 3611	. . . . . . 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 2797	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)})
20		df-uni 4857	. 2 ⊢ ∪ {𝐴, 𝐵} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})}
21		df-un 3902	. 2 ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
22	19, 20, 21	3eqtr4g 2791	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541  ∃wex 1780   ∈ wcel 2111  {cab 2709   ∪ cun 3895  {cpr 4575  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576  df-uni 4857

This theorem is referenced by:  unipr  4873  unisng  4874  unexg  7676  wunun  10601  tskun  10677  gruun  10697  mrcun  17528  unopn  22818  indistopon  22916  unconn  23344  limcun  25823  sshjval3  31334  prsiga  34144  unelsiga  34147  unelldsys  34171  measxun2  34223  measssd  34228  carsgsigalem  34328  carsgclctun  34334  pmeasmono  34337  probun  34432  indispconn  35278  bj-prmoore  37159  kelac2  43168  onsucunipr  43475  onsucunitp  43476  oaun2  43484  oaun3  43485  mnuund  44381  fourierdlem70  46284  fourierdlem71  46285  saluncl  46425  prsal  46426  meadjun  46570  omeunle  46624  toplatjoin  49112