Theorem ineq1 4167

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3401   ∩ cin 3902

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910

This theorem is referenced by:  ineq2  4168  ineq12  4169  ineq1i  4170  ineq1d  4173  unineq  4242  dfrab3ss  4277  disjeq0  4410  inex1g  5266  reseq1  5940  sspred  6276  isofrlem  7296  qsdisj  8743  fiint  9239  elfiun  9345  dffi3  9346  inf3lema  9545  dfac5lem5  10049  kmlem12  10084  kmlem14  10086  fin23lem24  10244  fin23lem26  10247  fin23lem23  10248  fin23lem22  10249  fin23lem27  10250  ingru  10738  uzin2  15280  incexclem  15771  elrestr  17360  firest  17364  rngcval  20563  ringcval  20592  inopn  22855  isbasisg  22903  basis1  22906  basis2  22907  tgval  22911  fctop  22960  cctop  22962  ntrfval  22980  elcls  23029  clsndisj  23031  elcls3  23039  neindisj2  23079  tgrest  23115  restco  23120  restsn  23126  restcld  23128  restcldi  23129  restopnb  23131  neitr  23136  restcls  23137  ordtbaslem  23144  ordtrest2lem  23159  hausnei2  23309  cnhaus  23310  regsep2  23332  dishaus  23338  ordthauslem  23339  cmpsublem  23355  cmpsub  23356  nconnsubb  23379  connsubclo  23380  1stcelcls  23417  islly  23424  cldllycmp  23451  lly1stc  23452  locfincmp  23482  elkgen  23492  ptclsg  23571  dfac14lem  23573  txrest  23587  pthaus  23594  txhaus  23603  xkohaus  23609  xkoptsub  23610  regr1lem  23695  isfbas  23785  fbasssin  23792  fbun  23796  isfil  23803  fbunfip  23825  fgval  23826  filconn  23839  uzrest  23853  isufil2  23864  hauspwpwf1  23943  fclsopni  23971  fclsnei  23975  fclsrest  23980  fcfnei  23991  fcfneii  23993  tsmsfbas  24084  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  ust0  24176  trust  24185  restutopopn  24194  lpbl  24459  methaus  24476  metrest  24480  restmetu  24526  qtopbaslem  24714  qdensere  24725  xrtgioo  24763  metnrmlem3  24818  icoopnst  24904  iocopnst  24905  ovolicc2lem2  25487  ovolicc2lem5  25490  mblsplit  25501  limcnlp  25847  ellimc3  25848  limcflf  25850  limciun  25863  ig1pval  26149  shincl  31469  shmodi  31478  omlsi  31492  pjoml  31524  chm0  31579  chincl  31587  chdmm1  31613  ledi  31628  cmbr  31672  cmbr3  31696  mdbr  32382  dmdmd  32388  dmdi  32390  dmdbr3  32393  dmdbr4  32394  mdslmd1lem4  32416  cvmd  32424  cvexch  32462  dmdbr6ati  32511  mddmdin0i  32519  difeq  32605  ofpreima2  32756  ssdifidlprm  33551  ufdprmidl  33634  1arithufdlem4  33640  rspectopn  34045  ordtrest2NEWlem  34100  inelsros  34356  diffiunisros  34357  measvuni  34392  measinb  34399  inelcarsg  34489  carsgclctunlem2  34497  totprob  34605  ballotlemgval  34702  noinfepfnregs  35310  cvmscbv  35474  cvmsdisj  35486  cvmsss2  35490  satfv1  35579  nepss  35934  brapply  36152  opnbnd  36541  isfne  36555  tailfb  36593  bj-restsn  37335  bj-restpw  37345  bj-rest0  37346  bj-restb  37347  nlpfvineqsn  37664  fvineqsnf1  37665  pibt2  37672  ptrest  37870  poimirlem30  37901  mblfinlem2  37909  bndss  38037  qsdisjALTV  38950  redundss3  38963  lcvexchlem4  39413  fipjust  43921  ntrkbimka  44394  ntrk0kbimka  44395  clsk3nimkb  44396  isotone2  44405  ntrclskb  44425  ntrclsk3  44426  ntrclsk13  44427  ismnushort  44657  relpfrlem  45309  permac8prim  45370  elrestd  45467  restsubel  45512  islptre  45979  islpcn  45997  subsaliuncllem  46715  subsaliuncl  46716  nnfoctbdjlem  46813  caragensplit  46858  vonvolmbllem  47018  vonvolmbl  47019  incsmflem  47099  decsmflem  47124  smflimlem2  47130  smflimlem3  47131  smflim  47135  smfpimcclem  47165  uzlidlring  48595  rngcvalALTV  48625  ringcvalALTV  48649  sepfsepc  49287  iscnrm3rlem2  49300  iscnrm3rlem8  49306  iscnrm3llem2  49309