Theorem ineq1 3840

Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)

Assertion

Ref	Expression
ineq1	⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Proof of Theorem ineq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2719	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 741	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3829	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3829	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 303	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	eqrdv 2649	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ∩ cin 3606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614

This theorem is referenced by:  ineq2  3841  ineq12  3842  ineq1i  3843  ineq1d  3846  unineq  3910  dfrab3ss  3938  intprg  4543  inex1g  4834  reseq1  5422  sspred  5726  isofrlem  6630  qsdisj  7867  fiint  8278  elfiun  8377  dffi3  8378  inf3lema  8559  dfac5lem5  8988  kmlem12  9021  kmlem14  9023  fin23lem24  9182  fin23lem26  9185  fin23lem23  9186  fin23lem22  9187  fin23lem27  9188  ingru  9675  uzin2  14128  incexclem  14612  elrestr  16136  firest  16140  inopn  20752  isbasisg  20799  basis1  20802  basis2  20803  tgval  20807  fctop  20856  cctop  20858  ntrfval  20876  elcls  20925  clsndisj  20927  elcls3  20935  neindisj2  20975  tgrest  21011  restco  21016  restsn  21022  restcld  21024  restcldi  21025  restopnb  21027  neitr  21032  restcls  21033  ordtbaslem  21040  ordtrest2lem  21055  hausnei2  21205  cnhaus  21206  regsep2  21228  dishaus  21234  ordthauslem  21235  cmpsublem  21250  cmpsub  21251  nconnsubb  21274  connsubclo  21275  1stcelcls  21312  islly  21319  cldllycmp  21346  lly1stc  21347  locfincmp  21377  elkgen  21387  ptclsg  21466  dfac14lem  21468  txrest  21482  pthaus  21489  txhaus  21498  xkohaus  21504  xkoptsub  21505  regr1lem  21590  isfbas  21680  fbasssin  21687  fbun  21691  isfil  21698  fbunfip  21720  fgval  21721  filconn  21734  uzrest  21748  isufil2  21759  hauspwpwf1  21838  fclsopni  21866  fclsnei  21870  fclsrest  21875  fcfnei  21886  fcfneii  21888  tsmsfbas  21978  ustincl  22058  ustdiag  22059  ustinvel  22060  ustexhalf  22061  ust0  22070  trust  22080  restutopopn  22089  lpbl  22355  methaus  22372  metrest  22376  restmetu  22422  qtopbaslem  22609  qdensere  22620  xrtgioo  22656  metnrmlem3  22711  icoopnst  22785  iocopnst  22786  ovolicc2lem2  23332  ovolicc2lem5  23335  mblsplit  23346  limcnlp  23687  ellimc3  23688  limcflf  23690  limciun  23703  ig1pval  23977  shincl  28368  shmodi  28377  omlsi  28391  pjoml  28423  chm0  28478  chincl  28486  chdmm1  28512  ledi  28527  cmbr  28571  cmbr3  28595  mdbr  29281  dmdmd  29287  dmdi  29289  dmdbr3  29292  dmdbr4  29293  mdslmd1lem4  29315  cvmd  29323  cvexch  29361  dmdbr6ati  29410  mddmdin0i  29418  difeq  29481  ofpreima2  29594  ordtrest2NEWlem  30096  inelsros  30369  diffiunisros  30370  measvuni  30405  measinb  30412  inelcarsg  30501  carsgclctunlem2  30509  totprob  30617  ballotlemgval  30713  cvmscbv  31366  cvmsdisj  31378  cvmsss2  31382  nepss  31725  brapply  32170  opnbnd  32445  isfne  32459  tailfb  32497  bj-restsn  33160  bj-restpw  33170  bj-rest0  33171  bj-restb  33172  ptrest  33538  poimirlem30  33569  mblfinlem2  33577  bndss  33715  lcvexchlem4  34642  fipjust  38187  ntrkbimka  38653  ntrk0kbimka  38654  clsk3nimkb  38655  isotone2  38664  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  elrestd  39605  islptre  40169  islpcn  40189  subsaliuncllem  40893  subsaliuncl  40894  nnfoctbdjlem  40990  caragensplit  41035  vonvolmbllem  41195  vonvolmbl  41196  incsmflem  41271  decsmflem  41295  smflimlem2  41301  smflimlem3  41302  smflim  41306  smfpimcclem  41334  uzlidlring  42254  rngcvalALTV  42286  rngcval  42287  ringcvalALTV  42332  ringcval  42333