Theorem uneq1 3956

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 2865	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 941	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 3949	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 3949	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 306	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2795	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 874   = wceq 1653   ∈ wcel 2157   ∪ cun 3765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-un 3772

This theorem is referenced by:  uneq2  3957  uneq12  3958  uneq1i  3959  uneq1d  3962  unineq  4076  prprc1  4487  uniprg  4640  relresfld  5879  unexb  7190  oarec  7880  xpider  8054  ralxpmap  8145  undifixp  8182  unxpdom  8407  enp1ilem  8434  findcard2  8440  domunfican  8473  pwfilem  8500  fin1a2lem10  9517  incexclem  14903  lcmfunsnlem  15686  ramub1lem1  16060  ramub1  16062  mreexexlem3d  16618  mreexexlem4d  16619  ipodrsima  17477  mplsubglem  19754  mretopd  21222  iscldtop  21225  nconnsubb  21552  plyval  24287  spanun  28921  difeq  29865  unelldsys  30729  isros  30739  unelros  30742  difelros  30743  rossros  30751  measun  30782  inelcarsg  30881  actfunsnf1o  31194  actfunsnrndisj  31195  mrsubvrs  31928  altopthsn  32573  rankung  32778  poimirlem28  33918  islshp  34992  lshpset2N  35132  paddval  35811  nacsfix  38049  eldioph4b  38149  eldioph4i  38150  diophren  38151  clsk3nimkb  39108  isotone1  39116  compneOLD  39413  fiiuncl  39981  founiiun0  40119  infxrpnf  40405  meadjun  41410  hoidmvle  41548