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  38872  redundss3  38885  lcvexchlem4  39297  fipjust  43806  ntrkbimka  44279  ntrk0kbimka  44280  clsk3nimkb  44281  isotone2  44290  ntrclskb  44310  ntrclsk3  44311  ntrclsk13  44312  ismnushort  44542  relpfrlem  45194  permac8prim  45255  elrestd  45352  restsubel  45397  islptre  45865  islpcn  45883  subsaliuncllem  46601  subsaliuncl  46602  nnfoctbdjlem  46699  caragensplit  46744  vonvolmbllem  46904  vonvolmbl  46905  incsmflem  46985  decsmflem  47010  smflimlem2  47016  smflimlem3  47017  smflim  47021  smfpimcclem  47051  uzlidlring  48481  rngcvalALTV  48511  ringcvalALTV  48535  sepfsepc  49173  iscnrm3rlem2  49186  iscnrm3rlem8  49192  iscnrm3llem2  49195