Theorem ineq1 4164

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3394   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-in 3910

This theorem is referenced by:  ineq2  4165  ineq12  4166  ineq1i  4167  ineq1d  4170  unineq  4239  dfrab3ss  4274  disjeq0  4407  inex1g  5258  reseq1  5924  sspred  6258  isofrlem  7277  qsdisj  8721  fiint  9216  fiintOLD  9217  elfiun  9320  dffi3  9321  inf3lema  9520  dfac5lem5  10021  kmlem12  10056  kmlem14  10058  fin23lem24  10216  fin23lem26  10219  fin23lem23  10220  fin23lem22  10221  fin23lem27  10222  ingru  10709  uzin2  15252  incexclem  15743  elrestr  17332  firest  17336  rngcval  20503  ringcval  20532  inopn  22784  isbasisg  22832  basis1  22835  basis2  22836  tgval  22840  fctop  22889  cctop  22891  ntrfval  22909  elcls  22958  clsndisj  22960  elcls3  22968  neindisj2  23008  tgrest  23044  restco  23049  restsn  23055  restcld  23057  restcldi  23058  restopnb  23060  neitr  23065  restcls  23066  ordtbaslem  23073  ordtrest2lem  23088  hausnei2  23238  cnhaus  23239  regsep2  23261  dishaus  23267  ordthauslem  23268  cmpsublem  23284  cmpsub  23285  nconnsubb  23308  connsubclo  23309  1stcelcls  23346  islly  23353  cldllycmp  23380  lly1stc  23381  locfincmp  23411  elkgen  23421  ptclsg  23500  dfac14lem  23502  txrest  23516  pthaus  23523  txhaus  23532  xkohaus  23538  xkoptsub  23539  regr1lem  23624  isfbas  23714  fbasssin  23721  fbun  23725  isfil  23732  fbunfip  23754  fgval  23755  filconn  23768  uzrest  23782  isufil2  23793  hauspwpwf1  23872  fclsopni  23900  fclsnei  23904  fclsrest  23909  fcfnei  23920  fcfneii  23922  tsmsfbas  24013  ustincl  24093  ustdiag  24094  ustinvel  24095  ustexhalf  24096  ust0  24105  trust  24115  restutopopn  24124  lpbl  24389  methaus  24406  metrest  24410  restmetu  24456  qtopbaslem  24644  qdensere  24655  xrtgioo  24693  metnrmlem3  24748  icoopnst  24834  iocopnst  24835  ovolicc2lem2  25417  ovolicc2lem5  25420  mblsplit  25431  limcnlp  25777  ellimc3  25778  limcflf  25780  limciun  25793  ig1pval  26079  shincl  31325  shmodi  31334  omlsi  31348  pjoml  31380  chm0  31435  chincl  31443  chdmm1  31469  ledi  31484  cmbr  31528  cmbr3  31552  mdbr  32238  dmdmd  32244  dmdi  32246  dmdbr3  32249  dmdbr4  32250  mdslmd1lem4  32272  cvmd  32280  cvexch  32318  dmdbr6ati  32367  mddmdin0i  32375  difeq  32462  ofpreima2  32609  ssdifidlprm  33395  ufdprmidl  33478  1arithufdlem4  33484  rspectopn  33834  ordtrest2NEWlem  33889  inelsros  34145  diffiunisros  34146  measvuni  34181  measinb  34188  inelcarsg  34279  carsgclctunlem2  34287  totprob  34395  ballotlemgval  34492  cvmscbv  35231  cvmsdisj  35243  cvmsss2  35247  satfv1  35336  nepss  35691  brapply  35912  opnbnd  36299  isfne  36313  tailfb  36351  bj-restsn  37056  bj-restpw  37066  bj-rest0  37067  bj-restb  37068  nlpfvineqsn  37383  fvineqsnf1  37384  pibt2  37391  ptrest  37599  poimirlem30  37630  mblfinlem2  37638  bndss  37766  qsdisjALTV  38592  redundss3  38605  lcvexchlem4  39016  fipjust  43538  ntrkbimka  44011  ntrk0kbimka  44012  clsk3nimkb  44013  isotone2  44022  ntrclskb  44042  ntrclsk3  44043  ntrclsk13  44044  ismnushort  44274  relpfrlem  44927  permac8prim  44988  elrestd  45086  restsubel  45131  islptre  45600  islpcn  45620  subsaliuncllem  46338  subsaliuncl  46339  nnfoctbdjlem  46436  caragensplit  46481  vonvolmbllem  46641  vonvolmbl  46642  incsmflem  46722  decsmflem  46747  smflimlem2  46753  smflimlem3  46754  smflim  46758  smfpimcclem  46788  uzlidlring  48219  rngcvalALTV  48249  ringcvalALTV  48273  sepfsepc  48912  iscnrm3rlem2  48925  iscnrm3rlem8  48931  iscnrm3llem2  48934