Theorem uniprg 4892

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 4893 to prove it from uniprg 4892. (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 3467	. . . . . . . . 9 ⊢ 𝑦 ∈ V
2	1	elpr 4619	. . . . . . . 8 ⊢ (𝑦 ∈ {𝐴, 𝐵} ↔ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵))
3	2	anbi2i 634	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)))
4		ancom 465	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ∧ 𝑥 ∈ 𝑦))
5		andir 1024	. . . . . . . 8 ⊢ (((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ∧ 𝑥 ∈ 𝑦) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
6	4, 5	bitri 278	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
7	3, 6	bitri 278	. . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
8	7	exbii 1875	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ ∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
9		19.43 1909	. . . . 5 ⊢ (∃𝑦((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
10	8, 9	bitri 278	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
11		clel3g 3629	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)))
12	11	bicomd 226	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
13	12	adantr 485	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐴))
14		clel3g 3629	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)))
15	14	bicomd 226	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → (∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐵))
16	15	adantl 486	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦) ↔ 𝑥 ∈ 𝐵))
17	13, 16	orbi12d 931	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦) ∨ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
18	10, 17	bitrid 286	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
19	18	abbidv 2835	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)})
20		df-uni 4877	. 2 ⊢ ∪ {𝐴, 𝐵} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ {𝐴, 𝐵})}
21		df-un 3918	. 2 ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
22	19, 20, 21	3eqtr4g 2829	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567  ∃wex 1806   ∈ wcel 2149  {cab 2747   ∪ cun 3911  {cpr 4596  ∪ cuni 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597  df-uni 4877

This theorem is referenced by:  unipr  4893  unisng  4894  unexg  7742  wunun  10695  tskun  10771  gruun  10791  mrcun  17678  unopn  23029  indistopon  23127  unconn  23555  limcun  26023  sshjval3  31647  prsiga  34466  unelsiga  34469  unelldsys  34493  measxun2  34545  measssd  34550  carsgsigalem  34650  carsgclctun  34656  pmeasmono  34659  probun  34754  indispconn  35659  bj-prmoore  37679  kelac2  43718  onsucunipr  44025  onsucunitp  44026  oaun2  44034  oaun3  44035  mnuund  44914  fourierdlem70  46816  fourierdlem71  46817  saluncl  46957  prsal  46958  meadjun  47102  omeunle  47156  toplatjoin  49699