Theorem ineq1 4110

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {crab 3412   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091

This theorem is used by:  ineq2  4111  ineq12  4112  ineq1i  4113  ineq1d  4116  unineq  4233  dfrab3ss  4268  disjeq0  4408  inex1g  5278  reseq1  5963  sspred  6313  isofrlem  7348  qsdisj  8815  fiint  9318  elfiun  9422  dffi3  9423  inf3lema  9625  dfac5lem5  10206  kmlem12  10240  kmlem14  10242  fin23lem24  10400  fin23lem26  10403  fin23lem23  10404  fin23lem22  10405  fin23lem27  10406  ingru  10900  uzin2  15512  incexclem  16005  elrestr  17599  firest  17603  rngcval  20870  ringcval  20899  ssdifidlprm  21642  inopn  23217  isbasisg  23265  basis1  23268  basis2  23269  tgval  23273  fctop  23322  cctop  23324  ntrfval  23342  elcls  23391  clsndisj  23393  elcls3  23401  neindisj2  23441  tgrest  23477  restco  23482  restsn  23488  restcld  23490  restcldi  23491  restopnb  23493  neitr  23498  restcls  23499  ordtbaslem  23506  ordtrest2lem  23521  hausnei2  23671  cnhaus  23672  regsep2  23694  dishaus  23700  ordthauslem  23701  cmpsublem  23717  cmpsub  23718  nconnsubb  23741  connsubclo  23742  1stcelcls  23780  islly  23787  cldllycmp  23814  lly1stc  23815  locfincmp  23845  elkgen  23855  ptclsg  23934  dfac14lem  23936  txrest  23950  pthaus  23957  txhaus  23966  xkohaus  23972  xkoptsub  23973  regr1lem  24058  isfbas  24148  fbasssin  24155  fbun  24159  isfil  24166  fbunfip  24188  fgval  24189  filconn  24202  uzrest  24216  isufil2  24227  hauspwpwf1  24306  fclsopni  24334  fclsnei  24338  fclsrest  24343  fcfnei  24354  fcfneii  24356  tsmsfbas  24447  ustincl  24527  ustdiag  24528  ustinvel  24529  ustexhalf  24530  ust0  24539  trust  24548  restutopopn  24557  lpbl  24822  methaus  24839  metrest  24843  restmetu  24889  qtopbaslem  25077  qdensere  25088  xrtgioo  25126  metnrmlem3  25181  icoopnst  25260  iocopnst  25261  ovolicc2lem2  25839  ovolicc2lem5  25842  mblsplit  25853  limcnlp  26198  ellimc3  26199  limcflf  26201  limciun  26214  ig1pval  26494  shincl  31983  shmodi  31992  omlsi  32006  pjoml  32038  chm0  32093  chincl  32101  chdmm1  32127  ledi  32142  cmbr  32186  cmbr3  32210  mdbr  32896  dmdmd  32902  dmdi  32904  dmdbr3  32907  dmdbr4  32908  mdslmd1lem4  32930  cvmd  32938  cvexch  32976  dmdbr6ati  33025  mddmdin0i  33033  difeq  33114  ofpreima2  33260  ufdprmidl  34073  1arithufdlem4  34079  rspectopn  34499  ordtrest2NEWlem  34554  inelsros  34811  diffiunisros  34812  measvuni  34847  measinb  34854  inelcarsg  34943  carsgclctunlem2  34951  totprob  35059  ballotlemgval  35156  noinfepfnregs  35800  cvmscbv  36023  cvmsdisj  36035  cvmsss2  36039  satfv1  36128  nepss  36483  brapply  36700  opnbnd  37113  isfne  37127  tailfb  37165  dfttc4  37318  elttcirr  37319  bj-restsn  38003  bj-restpw  38013  bj-rest0  38014  bj-restb  38015  nlpfvineqsn  38333  fvineqsnf1  38334  pibt2  38341  ptrest  38538  poimirlem30  38569  mblfinlem2  38577  bndss  38721  qsdisjALTV  39632  redundss3  39645  lcvexchlem4  40095  fipjust  44566  ntrkbimka  45038  ntrk0kbimka  45039  clsk3nimkb  45040  isotone2  45049  ntrclskb  45069  ntrclsk3  45070  ntrclsk13  45071  ismnushort  45285  relpfrlem  45943  permac8prim  46004  elrestd  46123  restsubel  46168  islptre  46631  islpcn  46649  subsaliuncllem  47367  subsaliuncl  47368  nnfoctbdjlem  47465  caragensplit  47510  vonvolmbllem  47670  vonvolmbl  47671  incsmflem  47751  decsmflem  47776  smflimlem2  47782  smflimlem3  47783  smflim  47787  smfpimcclem  47817  uzlidlring  49332  rngcvalALTV  49362  ringcvalALTV  49386  sepfsepc  50036  iscnrm3rlem2  50049  iscnrm3rlem8  50055  iscnrm3llem2  50058