Theorem ineq1 4165

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  {crab 3414   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3911

This theorem is referenced by:  ineq2  4166  ineq12  4167  ineq1i  4168  ineq1d  4171  unineq  4240  dfrab3ss  4275  disjeq0  4410  inex1g  5275  reseq1  5959  sspred  6297  isofrlem  7324  qsdisj  8776  fiint  9271  elfiun  9376  dffi3  9377  inf3lema  9579  dfac5lem5  10083  kmlem12  10118  kmlem14  10120  fin23lem24  10279  fin23lem26  10282  fin23lem23  10283  fin23lem22  10284  fin23lem27  10285  ingru  10773  uzin2  15372  incexclem  15866  elrestr  17457  firest  17461  rngcval  20668  ringcval  20697  inopn  22959  isbasisg  23007  basis1  23010  basis2  23011  tgval  23015  fctop  23064  cctop  23066  ntrfval  23084  elcls  23133  clsndisj  23135  elcls3  23143  neindisj2  23183  tgrest  23219  restco  23224  restsn  23230  restcld  23232  restcldi  23233  restopnb  23235  neitr  23240  restcls  23241  ordtbaslem  23248  ordtrest2lem  23263  hausnei2  23413  cnhaus  23414  regsep2  23436  dishaus  23442  ordthauslem  23443  cmpsublem  23459  cmpsub  23460  nconnsubb  23483  connsubclo  23484  1stcelcls  23521  islly  23528  cldllycmp  23555  lly1stc  23556  locfincmp  23586  elkgen  23596  ptclsg  23675  dfac14lem  23677  txrest  23691  pthaus  23698  txhaus  23707  xkohaus  23713  xkoptsub  23714  regr1lem  23799  isfbas  23889  fbasssin  23896  fbun  23900  isfil  23907  fbunfip  23929  fgval  23930  filconn  23943  uzrest  23957  isufil2  23968  hauspwpwf1  24047  fclsopni  24075  fclsnei  24079  fclsrest  24084  fcfnei  24095  fcfneii  24097  tsmsfbas  24188  ustincl  24268  ustdiag  24269  ustinvel  24270  ustexhalf  24271  ust0  24280  trust  24289  restutopopn  24298  lpbl  24563  methaus  24580  metrest  24584  restmetu  24630  qtopbaslem  24818  qdensere  24829  xrtgioo  24867  metnrmlem3  24922  icoopnst  25001  iocopnst  25002  ovolicc2lem2  25580  ovolicc2lem5  25583  mblsplit  25594  limcnlp  25940  ellimc3  25941  limcflf  25943  limciun  25956  ig1pval  26236  shincl  31584  shmodi  31593  omlsi  31607  pjoml  31639  chm0  31694  chincl  31702  chdmm1  31728  ledi  31743  cmbr  31787  cmbr3  31811  mdbr  32497  dmdmd  32503  dmdi  32505  dmdbr3  32508  dmdbr4  32509  mdslmd1lem4  32531  cvmd  32539  cvexch  32577  dmdbr6ati  32626  mddmdin0i  32634  difeq  32717  ofpreima2  32868  ssdifidlprm  33645  ufdprmidl  33737  1arithufdlem4  33743  rspectopn  34164  ordtrest2NEWlem  34219  inelsros  34475  diffiunisros  34476  measvuni  34511  measinb  34518  inelcarsg  34608  carsgclctunlem2  34616  totprob  34724  ballotlemgval  34821  noinfepfnregs  35428  cvmscbv  35608  cvmsdisj  35620  cvmsss2  35624  satfv1  35713  nepss  36068  brapply  36286  opnbnd  36685  isfne  36699  tailfb  36737  dfttc4  36890  elttcirr  36891  bj-restsn  37572  bj-restpw  37582  bj-rest0  37583  bj-restb  37584  nlpfvineqsn  37903  fvineqsnf1  37904  pibt2  37911  ptrest  38118  poimirlem30  38149  mblfinlem2  38157  bndss  38285  qsdisjALTV  39198  redundss3  39211  lcvexchlem4  39661  fipjust  44141  ntrkbimka  44614  ntrk0kbimka  44615  clsk3nimkb  44616  isotone2  44625  ntrclskb  44645  ntrclsk3  44646  ntrclsk13  44647  ismnushort  44877  relpfrlem  45529  permac8prim  45590  elrestd  45686  restsubel  45731  islptre  46195  islpcn  46213  subsaliuncllem  46931  subsaliuncl  46932  nnfoctbdjlem  47029  caragensplit  47074  vonvolmbllem  47234  vonvolmbl  47235  incsmflem  47315  decsmflem  47340  smflimlem2  47346  smflimlem3  47347  smflim  47351  smfpimcclem  47381  uzlidlring  48857  rngcvalALTV  48887  ringcvalALTV  48911  sepfsepc  49549  iscnrm3rlem2  49562  iscnrm3rlem8  49568  iscnrm3llem2  49571