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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3399   ∩ cin 3900

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  ineq2  4166  ineq12  4167  ineq1i  4168  ineq1d  4171  unineq  4240  dfrab3ss  4275  disjeq0  4408  inex1g  5264  reseq1  5932  sspred  6268  isofrlem  7286  qsdisj  8731  fiint  9227  elfiun  9333  dffi3  9334  inf3lema  9533  dfac5lem5  10037  kmlem12  10072  kmlem14  10074  fin23lem24  10232  fin23lem26  10235  fin23lem23  10236  fin23lem22  10237  fin23lem27  10238  ingru  10726  uzin2  15268  incexclem  15759  elrestr  17348  firest  17352  rngcval  20551  ringcval  20580  inopn  22843  isbasisg  22891  basis1  22894  basis2  22895  tgval  22899  fctop  22948  cctop  22950  ntrfval  22968  elcls  23017  clsndisj  23019  elcls3  23027  neindisj2  23067  tgrest  23103  restco  23108  restsn  23114  restcld  23116  restcldi  23117  restopnb  23119  neitr  23124  restcls  23125  ordtbaslem  23132  ordtrest2lem  23147  hausnei2  23297  cnhaus  23298  regsep2  23320  dishaus  23326  ordthauslem  23327  cmpsublem  23343  cmpsub  23344  nconnsubb  23367  connsubclo  23368  1stcelcls  23405  islly  23412  cldllycmp  23439  lly1stc  23440  locfincmp  23470  elkgen  23480  ptclsg  23559  dfac14lem  23561  txrest  23575  pthaus  23582  txhaus  23591  xkohaus  23597  xkoptsub  23598  regr1lem  23683  isfbas  23773  fbasssin  23780  fbun  23784  isfil  23791  fbunfip  23813  fgval  23814  filconn  23827  uzrest  23841  isufil2  23852  hauspwpwf1  23931  fclsopni  23959  fclsnei  23963  fclsrest  23968  fcfnei  23979  fcfneii  23981  tsmsfbas  24072  ustincl  24152  ustdiag  24153  ustinvel  24154  ustexhalf  24155  ust0  24164  trust  24173  restutopopn  24182  lpbl  24447  methaus  24464  metrest  24468  restmetu  24514  qtopbaslem  24702  qdensere  24713  xrtgioo  24751  metnrmlem3  24806  icoopnst  24892  iocopnst  24893  ovolicc2lem2  25475  ovolicc2lem5  25478  mblsplit  25489  limcnlp  25835  ellimc3  25836  limcflf  25838  limciun  25851  ig1pval  26137  shincl  31456  shmodi  31465  omlsi  31479  pjoml  31511  chm0  31566  chincl  31574  chdmm1  31600  ledi  31615  cmbr  31659  cmbr3  31683  mdbr  32369  dmdmd  32375  dmdi  32377  dmdbr3  32380  dmdbr4  32381  mdslmd1lem4  32403  cvmd  32411  cvexch  32449  dmdbr6ati  32498  mddmdin0i  32506  difeq  32593  ofpreima2  32744  ssdifidlprm  33539  ufdprmidl  33622  1arithufdlem4  33628  rspectopn  34024  ordtrest2NEWlem  34079  inelsros  34335  diffiunisros  34336  measvuni  34371  measinb  34378  inelcarsg  34468  carsgclctunlem2  34476  totprob  34584  ballotlemgval  34681  noinfepfnregs  35288  cvmscbv  35452  cvmsdisj  35464  cvmsss2  35468  satfv1  35557  nepss  35912  brapply  36130  opnbnd  36519  isfne  36533  tailfb  36571  bj-restsn  37287  bj-restpw  37297  bj-rest0  37298  bj-restb  37299  nlpfvineqsn  37614  fvineqsnf1  37615  pibt2  37622  ptrest  37820  poimirlem30  37851  mblfinlem2  37859  bndss  37987  qsdisjALTV  38882  redundss3  38895  lcvexchlem4  39307  fipjust  43816  ntrkbimka  44289  ntrk0kbimka  44290  clsk3nimkb  44291  isotone2  44300  ntrclskb  44320  ntrclsk3  44321  ntrclsk13  44322  ismnushort  44552  relpfrlem  45204  permac8prim  45265  elrestd  45362  restsubel  45407  islptre  45875  islpcn  45893  subsaliuncllem  46611  subsaliuncl  46612  nnfoctbdjlem  46709  caragensplit  46754  vonvolmbllem  46914  vonvolmbl  46915  incsmflem  46995  decsmflem  47020  smflimlem2  47026  smflimlem3  47027  smflim  47031  smfpimcclem  47061  uzlidlring  48491  rngcvalALTV  48521  ringcvalALTV  48545  sepfsepc  49183  iscnrm3rlem2  49196  iscnrm3rlem8  49202  iscnrm3llem2  49205