Theorem uneq1 4115

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 2852	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 929	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4107	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4107	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 317	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2761	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910

This theorem is referenced by:  uneq2  4116  uneq12  4117  uneq1i  4118  uneq1d  4121  unineq  4241  prprc1  4731  relresfld  6277  oarec  8543  xpider  8782  ralxpmap  8890  undifixp  8928  findcard2  9145  unxpdom  9215  enp1ilem  9234  pwfilem  9273  domunfican  9277  fin1a2lem10  10388  incexclem  15886  lcmfunsnlem  16694  ramub1lem1  17081  ramub1  17083  mreexexlem3d  17697  mreexexlem4d  17698  ipodrsima  18592  mplsubglem  22148  mretopd  23249  iscldtop  23252  nconnsubb  23580  plyval  26350  spanun  31897  difeq  32864  unelldsys  34548  isros  34558  unelros  34561  difelros  34562  rossros  34570  measun  34601  inelcarsg  34701  actfunsnf1o  34991  actfunsnrndisj  34992  mrsubvrs  36014  altopthsn  36453  rankung  36658  bj-adjg1  37679  poimirlem28  38299  islshp  39753  lshpset2N  39893  paddval  40572  nacsfix  43443  eldioph4b  43538  eldioph4i  43539  diophren  43540  clsk3nimkb  44766  isotone1  44774  fiiuncl  45785  founiiun0  45908  infxrpnf  46160  meadjun  47176  hoidmvle  47314