Theorem ineq1 4131

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 3431	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶})
2		dfin5 3889	. 2 ⊢ (𝐴 ∩ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶}
3		dfin5 3889	. 2 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶}
4	1, 2, 3	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  {crab 3110   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888

This theorem is referenced by:  ineq2  4133  ineq12  4134  ineq1i  4135  ineq1d  4138  unineq  4204  dfrab3ss  4233  disjeq0  4363  intprg  4872  inex1g  5187  reseq1  5812  sspred  6124  isofrlem  7072  qsdisj  8357  fiint  8779  elfiun  8878  dffi3  8879  inf3lema  9071  dfac5lem5  9538  kmlem12  9572  kmlem14  9574  fin23lem24  9733  fin23lem26  9736  fin23lem23  9737  fin23lem22  9738  fin23lem27  9739  ingru  10226  uzin2  14696  incexclem  15183  elrestr  16694  firest  16698  inopn  21504  isbasisg  21552  basis1  21555  basis2  21556  tgval  21560  fctop  21609  cctop  21611  ntrfval  21629  elcls  21678  clsndisj  21680  elcls3  21688  neindisj2  21728  tgrest  21764  restco  21769  restsn  21775  restcld  21777  restcldi  21778  restopnb  21780  neitr  21785  restcls  21786  ordtbaslem  21793  ordtrest2lem  21808  hausnei2  21958  cnhaus  21959  regsep2  21981  dishaus  21987  ordthauslem  21988  cmpsublem  22004  cmpsub  22005  nconnsubb  22028  connsubclo  22029  1stcelcls  22066  islly  22073  cldllycmp  22100  lly1stc  22101  locfincmp  22131  elkgen  22141  ptclsg  22220  dfac14lem  22222  txrest  22236  pthaus  22243  txhaus  22252  xkohaus  22258  xkoptsub  22259  regr1lem  22344  isfbas  22434  fbasssin  22441  fbun  22445  isfil  22452  fbunfip  22474  fgval  22475  filconn  22488  uzrest  22502  isufil2  22513  hauspwpwf1  22592  fclsopni  22620  fclsnei  22624  fclsrest  22629  fcfnei  22640  fcfneii  22642  tsmsfbas  22733  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  ust0  22825  trust  22835  restutopopn  22844  lpbl  23110  methaus  23127  metrest  23131  restmetu  23177  qtopbaslem  23364  qdensere  23375  xrtgioo  23411  metnrmlem3  23466  icoopnst  23544  iocopnst  23545  ovolicc2lem2  24122  ovolicc2lem5  24125  mblsplit  24136  limcnlp  24481  ellimc3  24482  limcflf  24484  limciun  24497  ig1pval  24773  shincl  29164  shmodi  29173  omlsi  29187  pjoml  29219  chm0  29274  chincl  29282  chdmm1  29308  ledi  29323  cmbr  29367  cmbr3  29391  mdbr  30077  dmdmd  30083  dmdi  30085  dmdbr3  30088  dmdbr4  30089  mdslmd1lem4  30111  cvmd  30119  cvexch  30157  dmdbr6ati  30206  mddmdin0i  30214  difeq  30289  ofpreima2  30429  rspectopn  31220  ordtrest2NEWlem  31275  inelsros  31547  diffiunisros  31548  measvuni  31583  measinb  31590  inelcarsg  31679  carsgclctunlem2  31687  totprob  31795  ballotlemgval  31891  cvmscbv  32618  cvmsdisj  32630  cvmsss2  32634  satfv1  32723  nepss  33061  brapply  33512  opnbnd  33786  isfne  33800  tailfb  33838  bj-restsn  34497  bj-restpw  34507  bj-rest0  34508  bj-restb  34509  nlpfvineqsn  34826  fvineqsnf1  34827  pibt2  34834  ptrest  35056  poimirlem30  35087  mblfinlem2  35095  bndss  35224  qsdisjALTV  36010  redundss3  36023  lcvexchlem4  36333  fipjust  40264  ntrkbimka  40741  ntrk0kbimka  40742  clsk3nimkb  40743  isotone2  40752  ntrclskb  40772  ntrclsk3  40773  ntrclsk13  40774  elrestd  41744  islptre  42261  islpcn  42281  subsaliuncllem  42997  subsaliuncl  42998  nnfoctbdjlem  43094  caragensplit  43139  vonvolmbllem  43299  vonvolmbl  43300  incsmflem  43375  decsmflem  43399  smflimlem2  43405  smflimlem3  43406  smflim  43410  smfpimcclem  43438  uzlidlring  44553  rngcvalALTV  44585  rngcval  44586  ringcvalALTV  44631  ringcval  44632