Theorem ineq1 4206

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  {crab 3433   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3956

This theorem is referenced by:  ineq2  4207  ineq12  4208  ineq1i  4209  ineq1d  4212  unineq  4278  dfrab3ss  4313  disjeq0  4456  intprgOLD  4989  inex1g  5320  reseq1  5976  sspred  6310  isofrlem  7337  qsdisj  8788  fiint  9324  elfiun  9425  dffi3  9426  inf3lema  9619  dfac5lem5  10122  kmlem12  10156  kmlem14  10158  fin23lem24  10317  fin23lem26  10320  fin23lem23  10321  fin23lem22  10322  fin23lem27  10323  ingru  10810  uzin2  15291  incexclem  15782  elrestr  17374  firest  17378  inopn  22401  isbasisg  22450  basis1  22453  basis2  22454  tgval  22458  fctop  22507  cctop  22509  ntrfval  22528  elcls  22577  clsndisj  22579  elcls3  22587  neindisj2  22627  tgrest  22663  restco  22668  restsn  22674  restcld  22676  restcldi  22677  restopnb  22679  neitr  22684  restcls  22685  ordtbaslem  22692  ordtrest2lem  22707  hausnei2  22857  cnhaus  22858  regsep2  22880  dishaus  22886  ordthauslem  22887  cmpsublem  22903  cmpsub  22904  nconnsubb  22927  connsubclo  22928  1stcelcls  22965  islly  22972  cldllycmp  22999  lly1stc  23000  locfincmp  23030  elkgen  23040  ptclsg  23119  dfac14lem  23121  txrest  23135  pthaus  23142  txhaus  23151  xkohaus  23157  xkoptsub  23158  regr1lem  23243  isfbas  23333  fbasssin  23340  fbun  23344  isfil  23351  fbunfip  23373  fgval  23374  filconn  23387  uzrest  23401  isufil2  23412  hauspwpwf1  23491  fclsopni  23519  fclsnei  23523  fclsrest  23528  fcfnei  23539  fcfneii  23541  tsmsfbas  23632  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  ust0  23724  trust  23734  restutopopn  23743  lpbl  24012  methaus  24029  metrest  24033  restmetu  24079  qtopbaslem  24275  qdensere  24286  xrtgioo  24322  metnrmlem3  24377  icoopnst  24455  iocopnst  24456  ovolicc2lem2  25035  ovolicc2lem5  25038  mblsplit  25049  limcnlp  25395  ellimc3  25396  limcflf  25398  limciun  25411  ig1pval  25690  shincl  30634  shmodi  30643  omlsi  30657  pjoml  30689  chm0  30744  chincl  30752  chdmm1  30778  ledi  30793  cmbr  30837  cmbr3  30861  mdbr  31547  dmdmd  31553  dmdi  31555  dmdbr3  31558  dmdbr4  31559  mdslmd1lem4  31581  cvmd  31589  cvexch  31627  dmdbr6ati  31676  mddmdin0i  31684  difeq  31756  ofpreima2  31891  rspectopn  32847  ordtrest2NEWlem  32902  inelsros  33176  diffiunisros  33177  measvuni  33212  measinb  33219  inelcarsg  33310  carsgclctunlem2  33318  totprob  33426  ballotlemgval  33522  cvmscbv  34249  cvmsdisj  34261  cvmsss2  34265  satfv1  34354  nepss  34687  brapply  34910  opnbnd  35210  isfne  35224  tailfb  35262  bj-restsn  35963  bj-restpw  35973  bj-rest0  35974  bj-restb  35975  nlpfvineqsn  36290  fvineqsnf1  36291  pibt2  36298  ptrest  36487  poimirlem30  36518  mblfinlem2  36526  bndss  36654  qsdisjALTV  37485  redundss3  37498  lcvexchlem4  37907  fipjust  42316  ntrkbimka  42789  ntrk0kbimka  42790  clsk3nimkb  42791  isotone2  42800  ntrclskb  42820  ntrclsk3  42821  ntrclsk13  42822  ismnushort  43060  elrestd  43797  restsubel  43847  islptre  44335  islpcn  44355  subsaliuncllem  45073  subsaliuncl  45074  nnfoctbdjlem  45171  caragensplit  45216  vonvolmbllem  45376  vonvolmbl  45377  incsmflem  45457  decsmflem  45482  smflimlem2  45488  smflimlem3  45489  smflim  45493  smfpimcclem  45523  uzlidlring  46827  rngcvalALTV  46859  rngcval  46860  ringcvalALTV  46905  ringcval  46906  sepfsepc  47560  iscnrm3rlem2  47574  iscnrm3rlem8  47580  iscnrm3llem2  47583