Theorem ineq1 4160

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  {crab 3395   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904

This theorem is referenced by:  ineq2  4161  ineq12  4162  ineq1i  4163  ineq1d  4166  unineq  4235  dfrab3ss  4270  disjeq0  4403  inex1g  5255  reseq1  5921  sspred  6257  isofrlem  7274  qsdisj  8718  fiint  9211  elfiun  9314  dffi3  9315  inf3lema  9514  dfac5lem5  10018  kmlem12  10053  kmlem14  10055  fin23lem24  10213  fin23lem26  10216  fin23lem23  10217  fin23lem22  10218  fin23lem27  10219  ingru  10706  uzin2  15252  incexclem  15743  elrestr  17332  firest  17336  rngcval  20533  ringcval  20562  inopn  22814  isbasisg  22862  basis1  22865  basis2  22866  tgval  22870  fctop  22919  cctop  22921  ntrfval  22939  elcls  22988  clsndisj  22990  elcls3  22998  neindisj2  23038  tgrest  23074  restco  23079  restsn  23085  restcld  23087  restcldi  23088  restopnb  23090  neitr  23095  restcls  23096  ordtbaslem  23103  ordtrest2lem  23118  hausnei2  23268  cnhaus  23269  regsep2  23291  dishaus  23297  ordthauslem  23298  cmpsublem  23314  cmpsub  23315  nconnsubb  23338  connsubclo  23339  1stcelcls  23376  islly  23383  cldllycmp  23410  lly1stc  23411  locfincmp  23441  elkgen  23451  ptclsg  23530  dfac14lem  23532  txrest  23546  pthaus  23553  txhaus  23562  xkohaus  23568  xkoptsub  23569  regr1lem  23654  isfbas  23744  fbasssin  23751  fbun  23755  isfil  23762  fbunfip  23784  fgval  23785  filconn  23798  uzrest  23812  isufil2  23823  hauspwpwf1  23902  fclsopni  23930  fclsnei  23934  fclsrest  23939  fcfnei  23950  fcfneii  23952  tsmsfbas  24043  ustincl  24123  ustdiag  24124  ustinvel  24125  ustexhalf  24126  ust0  24135  trust  24144  restutopopn  24153  lpbl  24418  methaus  24435  metrest  24439  restmetu  24485  qtopbaslem  24673  qdensere  24684  xrtgioo  24722  metnrmlem3  24777  icoopnst  24863  iocopnst  24864  ovolicc2lem2  25446  ovolicc2lem5  25449  mblsplit  25460  limcnlp  25806  ellimc3  25807  limcflf  25809  limciun  25822  ig1pval  26108  shincl  31361  shmodi  31370  omlsi  31384  pjoml  31416  chm0  31471  chincl  31479  chdmm1  31505  ledi  31520  cmbr  31564  cmbr3  31588  mdbr  32274  dmdmd  32280  dmdi  32282  dmdbr3  32285  dmdbr4  32286  mdslmd1lem4  32308  cvmd  32316  cvexch  32354  dmdbr6ati  32403  mddmdin0i  32411  difeq  32498  ofpreima2  32648  ssdifidlprm  33423  ufdprmidl  33506  1arithufdlem4  33512  rspectopn  33880  ordtrest2NEWlem  33935  inelsros  34191  diffiunisros  34192  measvuni  34227  measinb  34234  inelcarsg  34324  carsgclctunlem2  34332  totprob  34440  ballotlemgval  34537  cvmscbv  35302  cvmsdisj  35314  cvmsss2  35318  satfv1  35407  nepss  35762  brapply  35980  opnbnd  36367  isfne  36381  tailfb  36419  bj-restsn  37124  bj-restpw  37134  bj-rest0  37135  bj-restb  37136  nlpfvineqsn  37451  fvineqsnf1  37452  pibt2  37459  ptrest  37667  poimirlem30  37698  mblfinlem2  37706  bndss  37834  qsdisjALTV  38660  redundss3  38673  lcvexchlem4  39084  fipjust  43606  ntrkbimka  44079  ntrk0kbimka  44080  clsk3nimkb  44081  isotone2  44090  ntrclskb  44110  ntrclsk3  44111  ntrclsk13  44112  ismnushort  44342  relpfrlem  44994  permac8prim  45055  elrestd  45153  restsubel  45198  islptre  45667  islpcn  45685  subsaliuncllem  46403  subsaliuncl  46404  nnfoctbdjlem  46501  caragensplit  46546  vonvolmbllem  46706  vonvolmbl  46707  incsmflem  46787  decsmflem  46812  smflimlem2  46818  smflimlem3  46819  smflim  46823  smfpimcclem  46853  uzlidlring  48274  rngcvalALTV  48304  ringcvalALTV  48328  sepfsepc  48967  iscnrm3rlem2  48980  iscnrm3rlem8  48986  iscnrm3llem2  48989