Theorem ineq1 4142

Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) (Proof shortened by SN, 20-Sep-2023.)

Assertion

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

Proof of Theorem ineq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabeq 3405	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶})
2		dfin5 3891	. 2 ⊢ (𝐴 ∩ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶}
3		dfin5 3891	. 2 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶}
4	1, 2, 3	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  {crab 3391   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  ineq2  4143  ineq12  4144  ineq1i  4145  ineq1d  4148  unineq  4216  dfrab3ss  4251  disjeq0  4384  inex1g  5247  reseq1  5925  sspred  6261  isofrlem  7284  qsdisj  8731  fiint  9227  elfiun  9333  dffi3  9334  inf3lema  9536  dfac5lem5  10040  kmlem12  10075  kmlem14  10077  fin23lem24  10235  fin23lem26  10238  fin23lem23  10239  fin23lem22  10240  fin23lem27  10241  ingru  10729  uzin2  15298  incexclem  15792  elrestr  17382  firest  17386  rngcval  20590  ringcval  20619  inopn  22882  isbasisg  22930  basis1  22933  basis2  22934  tgval  22938  fctop  22987  cctop  22989  ntrfval  23007  elcls  23056  clsndisj  23058  elcls3  23066  neindisj2  23106  tgrest  23142  restco  23147  restsn  23153  restcld  23155  restcldi  23156  restopnb  23158  neitr  23163  restcls  23164  ordtbaslem  23171  ordtrest2lem  23186  hausnei2  23336  cnhaus  23337  regsep2  23359  dishaus  23365  ordthauslem  23366  cmpsublem  23382  cmpsub  23383  nconnsubb  23406  connsubclo  23407  1stcelcls  23444  islly  23451  cldllycmp  23478  lly1stc  23479  locfincmp  23509  elkgen  23519  ptclsg  23598  dfac14lem  23600  txrest  23614  pthaus  23621  txhaus  23630  xkohaus  23636  xkoptsub  23637  regr1lem  23722  isfbas  23812  fbasssin  23819  fbun  23823  isfil  23830  fbunfip  23852  fgval  23853  filconn  23866  uzrest  23880  isufil2  23891  hauspwpwf1  23970  fclsopni  23998  fclsnei  24002  fclsrest  24007  fcfnei  24018  fcfneii  24020  tsmsfbas  24111  ustincl  24191  ustdiag  24192  ustinvel  24193  ustexhalf  24194  ust0  24203  trust  24212  restutopopn  24221  lpbl  24486  methaus  24503  metrest  24507  restmetu  24553  qtopbaslem  24741  qdensere  24752  xrtgioo  24790  metnrmlem3  24845  icoopnst  24924  iocopnst  24925  ovolicc2lem2  25503  ovolicc2lem5  25506  mblsplit  25517  limcnlp  25863  ellimc3  25864  limcflf  25866  limciun  25879  ig1pval  26159  shincl  31470  shmodi  31479  omlsi  31493  pjoml  31525  chm0  31580  chincl  31588  chdmm1  31614  ledi  31629  cmbr  31673  cmbr3  31697  mdbr  32383  dmdmd  32389  dmdi  32391  dmdbr3  32394  dmdbr4  32395  mdslmd1lem4  32417  cvmd  32425  cvexch  32463  dmdbr6ati  32512  mddmdin0i  32520  difeq  32606  ofpreima2  32758  ssdifidlprm  33541  ufdprmidl  33624  1arithufdlem4  33630  rspectopn  34051  ordtrest2NEWlem  34106  inelsros  34362  diffiunisros  34363  measvuni  34398  measinb  34405  inelcarsg  34495  carsgclctunlem2  34503  totprob  34611  ballotlemgval  34708  noinfepfnregs  35313  cvmscbv  35486  cvmsdisj  35498  cvmsss2  35502  satfv1  35591  nepss  35946  brapply  36164  opnbnd  36553  isfne  36567  tailfb  36605  dfttc4  36758  elttcirr  36759  bj-restsn  37440  bj-restpw  37450  bj-rest0  37451  bj-restb  37452  nlpfvineqsn  37771  fvineqsnf1  37772  pibt2  37779  ptrest  37986  poimirlem30  38017  mblfinlem2  38025  bndss  38153  qsdisjALTV  39066  redundss3  39079  lcvexchlem4  39529  fipjust  44009  ntrkbimka  44482  ntrk0kbimka  44483  clsk3nimkb  44484  isotone2  44493  ntrclskb  44513  ntrclsk3  44514  ntrclsk13  44515  ismnushort  44745  relpfrlem  45397  permac8prim  45458  elrestd  45555  restsubel  45600  islptre  46064  islpcn  46082  subsaliuncllem  46800  subsaliuncl  46801  nnfoctbdjlem  46898  caragensplit  46943  vonvolmbllem  47103  vonvolmbl  47104  incsmflem  47184  decsmflem  47209  smflimlem2  47215  smflimlem3  47216  smflim  47220  smfpimcclem  47250  uzlidlring  48726  rngcvalALTV  48756  ringcvalALTV  48780  sepfsepc  49418  iscnrm3rlem2  49431  iscnrm3rlem8  49437  iscnrm3llem2  49440