Theorem uniprg 4880

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 4881 to prove it from uniprg 4880. (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 3445	. . . . . . . . 9 ⊢ 𝑦 ∈ V
2	1	elpr 4606	. . . . . . . 8 ⊢ (𝑦 ∈ {𝐴, 𝐵} ↔ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵))
3	2	anbi2i 624	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)))
4		ancom 460	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ∧ 𝑥 ∈ 𝑦))
5		andir 1011	. . . . . . . 8 ⊢ (((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ∧ 𝑥 ∈ 𝑦) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
6	4, 5	bitri 275	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
7	3, 6	bitri 275	. . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
8	7	exbii 1850	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
9		19.43 1884	. . . . 5 ⊢ (∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
10	8, 9	bitri 275	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
11		clel3g 3616	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)))
12	11	bicomd 223	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
13	12	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
14		clel3g 3616	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
15	14	bicomd 223	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → (∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐵))
16	15	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐵))
17	13, 16	orbi12d 919	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
18	10, 17	bitrid 283	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
19	18	abbidv 2803	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)})
20		df-uni 4865	. 2 ⊢ ∪ {𝐴, 𝐵} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})}
21		df-un 3907	. 2 ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
22	19, 20, 21	3eqtr4g 2797	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715   ∪ cun 3900  {cpr 4583  ∪ cuni 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-un 3907  df-sn 4582  df-pr 4584  df-uni 4865

This theorem is referenced by:  unipr  4881  unisng  4882  unexg  7690  wunun  10625  tskun  10701  gruun  10721  mrcun  17549  unopn  22851  indistopon  22949  unconn  23377  limcun  25856  sshjval3  31433  prsiga  34290  unelsiga  34293  unelldsys  34317  measxun2  34369  measssd  34374  carsgsigalem  34474  carsgclctun  34480  pmeasmono  34483  probun  34578  indispconn  35430  bj-prmoore  37322  kelac2  43374  onsucunipr  43681  onsucunitp  43682  oaun2  43690  oaun3  43691  mnuund  44586  fourierdlem70  46487  fourierdlem71  46488  saluncl  46628  prsal  46629  meadjun  46773  omeunle  46827  toplatjoin  49314