Theorem ineq1 4113

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {crab 3416   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094

This theorem is used by:  ineq2  4114  ineq12  4115  ineq1i  4116  ineq1d  4119  unineq  4236  dfrab3ss  4271  disjeq0  4412  inex1g  5286  reseq1  5980  sspred  6339  isofrlem  7379  qsdisj  8853  fiint  9356  elfiun  9459  dffi3  9460  inf3lema  9662  dfac5lem5  10245  kmlem12  10279  kmlem14  10281  fin23lem24  10439  fin23lem26  10442  fin23lem23  10443  fin23lem22  10444  fin23lem27  10445  ingru  10939  uzin2  15556  incexclem  16049  elrestr  17649  firest  17653  rngcval  20921  ringcval  20950  ssdifidlprm  21693  inopn  23272  isbasisg  23320  basis1  23323  basis2  23324  tgval  23328  fctop  23377  cctop  23379  ntrfval  23397  elcls  23446  clsndisj  23448  elcls3  23456  neindisj2  23496  tgrest  23532  restco  23537  restsn  23543  restcld  23545  restcldi  23546  restopnb  23548  neitr  23553  restcls  23554  ordtbaslem  23561  ordtrest2lem  23576  hausnei2  23726  cnhaus  23727  regsep2  23749  dishaus  23755  ordthauslem  23756  cmpsublem  23772  cmpsub  23773  nconnsubb  23796  connsubclo  23797  1stcelcls  23835  islly  23842  cldllycmp  23869  lly1stc  23870  locfincmp  23900  elkgen  23910  ptclsg  23989  dfac14lem  23991  txrest  24005  pthaus  24012  txhaus  24021  xkohaus  24027  xkoptsub  24028  regr1lem  24113  isfbas  24203  fbasssin  24210  fbun  24214  isfil  24221  fbunfip  24243  fgval  24244  filconn  24257  uzrest  24271  isufil2  24282  hauspwpwf1  24361  fclsopni  24389  fclsnei  24393  fclsrest  24398  fcfnei  24409  fcfneii  24411  tsmsfbas  24502  ustincl  24582  ustdiag  24583  ustinvel  24584  ustexhalf  24585  ust0  24594  trust  24603  restutopopn  24612  lpbl  24877  methaus  24894  metrest  24898  restmetu  24944  qtopbaslem  25132  qdensere  25143  xrtgioo  25181  metnrmlem3  25236  icoopnst  25315  iocopnst  25316  ovolicc2lem2  25894  ovolicc2lem5  25897  mblsplit  25908  limcnlp  26253  ellimc3  26254  limcflf  26256  limciun  26269  ig1pval  26549  shincl  32040  shmodi  32049  omlsi  32063  pjoml  32095  chm0  32150  chincl  32158  chdmm1  32184  ledi  32199  cmbr  32243  cmbr3  32267  mdbr  32953  dmdmd  32959  dmdi  32961  dmdbr3  32964  dmdbr4  32965  mdslmd1lem4  32987  cvmd  32995  cvexch  33033  dmdbr6ati  33082  mddmdin0i  33090  difeq  33213  ofpreima2  33358  ufdprmidl  34177  1arithufdlem4  34183  rspectopn  34610  ordtrest2NEWlem  34665  inelsros  34922  diffiunisros  34923  measvuni  34958  measinb  34965  inelcarsg  35054  carsgclctunlem2  35062  totprob  35170  ballotlemgval  35267  noinfepfnregs  35941  gdlop2fv  36005  gdlop5fv  36008  gdlop6fv  36009  gdlop7fv  36010  gdlop8fv  36011  cvmscbv  36231  cvmsdisj  36243  cvmsss2  36247  satfv1  36336  mirimanofffr  36670  nepss  36698  brapply  36915  opnbnd  37328  isfne  37342  tailfb  37380  dfttc4  37533  elttcirr  37534  bj-restsn  38273  bj-restpw  38283  bj-rest0  38284  bj-restb  38285  nlpfvineqsn  38600  fvineqsnf1  38601  pibt2  38608  ptrest  38805  poimirlem30  38836  mblfinlem2  38844  bndss  38986  qsdisjALTV  39897  redundss3  39910  lcvexchlem4  40360  fipjust  44827  ntrkbimka  45299  ntrk0kbimka  45300  clsk3nimkb  45301  isotone2  45310  ntrclskb  45330  ntrclsk3  45331  ntrclsk13  45332  ismnushort  45546  relpfrlem  46207  permac8prim  46268  elrestd  46396  restsubel  46441  islptre  46904  islpcn  46922  subsaliuncllem  47640  subsaliuncl  47641  nnfoctbdjlem  47738  caragensplit  47783  vonvolmbllem  47943  vonvolmbl  47944  incsmflem  48024  decsmflem  48049  smflimlem2  48055  smflimlem3  48056  smflim  48060  smfpimcclem  48090  uzlidlring  49605  rngcvalALTV  49635  ringcvalALTV  49659  sepfsepc  50373  iscnrm3rlem2  50386  iscnrm3rlem8  50392  iscnrm3llem2  50395