Theorem ineq1 4159

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3413   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906

This theorem is used by:  ineq2  4160  ineq12  4161  ineq1i  4162  ineq1d  4165  unineq  4234  dfrab3ss  4269  disjeq0  4409  inex1g  5279  reseq1  5964  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  38332  fvineqsnf1  38333  pibt2  38340  ptrest  38537  poimirlem30  38568  mblfinlem2  38576  bndss  38720  qsdisjALTV  39631  redundss3  39644  lcvexchlem4  40094  fipjust  44565  ntrkbimka  45037  ntrk0kbimka  45038  clsk3nimkb  45039  isotone2  45048  ntrclskb  45068  ntrclsk3  45069  ntrclsk13  45070  ismnushort  45284  relpfrlem  45942  permac8prim  46003  elrestd  46122  restsubel  46167  islptre  46630  islpcn  46648  subsaliuncllem  47366  subsaliuncl  47367  nnfoctbdjlem  47464  caragensplit  47509  vonvolmbllem  47669  vonvolmbl  47670  incsmflem  47750  decsmflem  47775  smflimlem2  47781  smflimlem3  47782  smflim  47786  smfpimcclem  47816  uzlidlring  49331  rngcvalALTV  49361  ringcvalALTV  49385  sepfsepc  50035  iscnrm3rlem2  50048  iscnrm3rlem8  50054  iscnrm3llem2  50057