Theorem uneq1 3722

Description: Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
uneq1	⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Proof of Theorem uneq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2677	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 735	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 3715	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 3715	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 302	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2608	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 382   = wceq 1475   ∈ wcel 1977   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545

This theorem is referenced by:  uneq2  3723  uneq12  3724  uneq1i  3725  uneq1d  3728  unineq  3836  prprc1  4243  uniprg  4386  relresfld  5579  unexb  6856  oarec  7529  xpider  7705  ralxpmap  7793  undifixp  7830  unxpdom  8052  enp1ilem  8079  findcard2  8085  domunfican  8118  pwfilem  8143  fin1a2lem10  9114  incexclem  14407  lcmfunsnlem  15192  ramub1lem1  15568  ramub1  15570  mreexexlem3d  16129  mreexexlem4d  16130  ipodrsima  16988  mplsubglem  19255  mretopd  20706  iscldtop  20709  nconsubb  21036  plyval  23753  spanun  27788  difeq  28739  unelldsys  29548  isros  29558  unelros  29561  difelros  29562  rossros  29570  measun  29601  inelcarsg  29700  mrsubvrs  30673  nofulllem2  31102  altopthsn  31238  rankung  31443  poimirlem28  32607  islshp  33284  lshpset2N  33424  paddval  34102  nacsfix  36293  eldioph4b  36393  eldioph4i  36394  diophren  36395  clsk3nimkb  37358  isotone1  37366  compne  37665  fiiuncl  38259  founiiun0  38372  meadjun  39355  hoidmvle  39490