Theorem ineq1 4204

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  {crab 3432   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3954

This theorem is referenced by:  ineq2  4205  ineq12  4206  ineq1i  4207  ineq1d  4210  unineq  4276  dfrab3ss  4311  disjeq0  4454  intprgOLD  4987  inex1g  5318  reseq1  5973  sspred  6306  isofrlem  7333  qsdisj  8784  fiint  9320  elfiun  9421  dffi3  9422  inf3lema  9615  dfac5lem5  10118  kmlem12  10152  kmlem14  10154  fin23lem24  10313  fin23lem26  10316  fin23lem23  10317  fin23lem22  10318  fin23lem27  10319  ingru  10806  uzin2  15287  incexclem  15778  elrestr  17370  firest  17374  inopn  22392  isbasisg  22441  basis1  22444  basis2  22445  tgval  22449  fctop  22498  cctop  22500  ntrfval  22519  elcls  22568  clsndisj  22570  elcls3  22578  neindisj2  22618  tgrest  22654  restco  22659  restsn  22665  restcld  22667  restcldi  22668  restopnb  22670  neitr  22675  restcls  22676  ordtbaslem  22683  ordtrest2lem  22698  hausnei2  22848  cnhaus  22849  regsep2  22871  dishaus  22877  ordthauslem  22878  cmpsublem  22894  cmpsub  22895  nconnsubb  22918  connsubclo  22919  1stcelcls  22956  islly  22963  cldllycmp  22990  lly1stc  22991  locfincmp  23021  elkgen  23031  ptclsg  23110  dfac14lem  23112  txrest  23126  pthaus  23133  txhaus  23142  xkohaus  23148  xkoptsub  23149  regr1lem  23234  isfbas  23324  fbasssin  23331  fbun  23335  isfil  23342  fbunfip  23364  fgval  23365  filconn  23378  uzrest  23392  isufil2  23403  hauspwpwf1  23482  fclsopni  23510  fclsnei  23514  fclsrest  23519  fcfnei  23530  fcfneii  23532  tsmsfbas  23623  ustincl  23703  ustdiag  23704  ustinvel  23705  ustexhalf  23706  ust0  23715  trust  23725  restutopopn  23734  lpbl  24003  methaus  24020  metrest  24024  restmetu  24070  qtopbaslem  24266  qdensere  24277  xrtgioo  24313  metnrmlem3  24368  icoopnst  24446  iocopnst  24447  ovolicc2lem2  25026  ovolicc2lem5  25029  mblsplit  25040  limcnlp  25386  ellimc3  25387  limcflf  25389  limciun  25402  ig1pval  25681  shincl  30621  shmodi  30630  omlsi  30644  pjoml  30676  chm0  30731  chincl  30739  chdmm1  30765  ledi  30780  cmbr  30824  cmbr3  30848  mdbr  31534  dmdmd  31540  dmdi  31542  dmdbr3  31545  dmdbr4  31546  mdslmd1lem4  31568  cvmd  31576  cvexch  31614  dmdbr6ati  31663  mddmdin0i  31671  difeq  31743  ofpreima2  31878  rspectopn  32835  ordtrest2NEWlem  32890  inelsros  33164  diffiunisros  33165  measvuni  33200  measinb  33207  inelcarsg  33298  carsgclctunlem2  33306  totprob  33414  ballotlemgval  33510  cvmscbv  34237  cvmsdisj  34249  cvmsss2  34253  satfv1  34342  nepss  34675  brapply  34898  opnbnd  35198  isfne  35212  tailfb  35250  bj-restsn  35951  bj-restpw  35961  bj-rest0  35962  bj-restb  35963  nlpfvineqsn  36278  fvineqsnf1  36279  pibt2  36286  ptrest  36475  poimirlem30  36506  mblfinlem2  36514  bndss  36642  qsdisjALTV  37473  redundss3  37486  lcvexchlem4  37895  fipjust  42301  ntrkbimka  42774  ntrk0kbimka  42775  clsk3nimkb  42776  isotone2  42785  ntrclskb  42805  ntrclsk3  42806  ntrclsk13  42807  ismnushort  43045  elrestd  43782  restsubel  43832  islptre  44321  islpcn  44341  subsaliuncllem  45059  subsaliuncl  45060  nnfoctbdjlem  45157  caragensplit  45202  vonvolmbllem  45362  vonvolmbl  45363  incsmflem  45443  decsmflem  45468  smflimlem2  45474  smflimlem3  45475  smflim  45479  smfpimcclem  45509  uzlidlring  46780  rngcvalALTV  46812  rngcval  46813  ringcvalALTV  46858  ringcval  46859  sepfsepc  47513  iscnrm3rlem2  47527  iscnrm3rlem8  47533  iscnrm3llem2  47536