Theorem ineq1 4166

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  {crab 3416   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3912

This theorem is referenced by:  ineq2  4167  ineq12  4168  ineq1i  4169  ineq1d  4172  unineq  4241  dfrab3ss  4276  disjeq0  4416  inex1g  5288  reseq1  5972  sspred  6311  isofrlem  7338  qsdisj  8788  fiint  9282  elfiun  9386  dffi3  9387  inf3lema  9589  dfac5lem5  10107  kmlem12  10141  kmlem14  10143  fin23lem24  10301  fin23lem26  10304  fin23lem23  10305  fin23lem22  10306  fin23lem27  10307  ingru  10795  uzin2  15392  incexclem  15886  elrestr  17476  firest  17480  rngcval  20717  ringcval  20746  ssdifidlprm  21486  inopn  23056  isbasisg  23104  basis1  23107  basis2  23108  tgval  23112  fctop  23161  cctop  23163  ntrfval  23181  elcls  23230  clsndisj  23232  elcls3  23240  neindisj2  23280  tgrest  23316  restco  23321  restsn  23327  restcld  23329  restcldi  23330  restopnb  23332  neitr  23337  restcls  23338  ordtbaslem  23345  ordtrest2lem  23360  hausnei2  23510  cnhaus  23511  regsep2  23533  dishaus  23539  ordthauslem  23540  cmpsublem  23556  cmpsub  23557  nconnsubb  23580  connsubclo  23581  1stcelcls  23618  islly  23625  cldllycmp  23652  lly1stc  23653  locfincmp  23683  elkgen  23693  ptclsg  23772  dfac14lem  23774  txrest  23788  pthaus  23795  txhaus  23804  xkohaus  23810  xkoptsub  23811  regr1lem  23896  isfbas  23986  fbasssin  23993  fbun  23997  isfil  24004  fbunfip  24026  fgval  24027  filconn  24040  uzrest  24054  isufil2  24065  hauspwpwf1  24144  fclsopni  24172  fclsnei  24176  fclsrest  24181  fcfnei  24192  fcfneii  24194  tsmsfbas  24285  ustincl  24365  ustdiag  24366  ustinvel  24367  ustexhalf  24368  ust0  24377  trust  24386  restutopopn  24395  lpbl  24660  methaus  24677  metrest  24681  restmetu  24727  qtopbaslem  24915  qdensere  24926  xrtgioo  24964  metnrmlem3  25019  icoopnst  25098  iocopnst  25099  ovolicc2lem2  25677  ovolicc2lem5  25680  mblsplit  25691  limcnlp  26037  ellimc3  26038  limcflf  26040  limciun  26053  ig1pval  26333  shincl  31733  shmodi  31742  omlsi  31756  pjoml  31788  chm0  31843  chincl  31851  chdmm1  31877  ledi  31892  cmbr  31936  cmbr3  31960  mdbr  32646  dmdmd  32652  dmdi  32654  dmdbr3  32657  dmdbr4  32658  mdslmd1lem4  32680  cvmd  32688  cvexch  32726  dmdbr6ati  32775  mddmdin0i  32783  difeq  32864  ofpreima2  33011  ufdprmidl  33831  1arithufdlem4  33837  rspectopn  34257  ordtrest2NEWlem  34312  inelsros  34568  diffiunisros  34569  measvuni  34604  measinb  34611  inelcarsg  34701  carsgclctunlem2  34709  totprob  34817  ballotlemgval  34914  noinfepfnregs  35545  cvmscbv  35750  cvmsdisj  35762  cvmsss2  35766  satfv1  35855  nepss  36210  brapply  36428  opnbnd  36836  isfne  36850  tailfb  36888  dfttc4  37041  elttcirr  37042  bj-restsn  37724  bj-restpw  37734  bj-rest0  37735  bj-restb  37736  nlpfvineqsn  38055  fvineqsnf1  38056  pibt2  38063  ptrest  38270  poimirlem30  38301  mblfinlem2  38309  bndss  38437  qsdisjALTV  39348  redundss3  39361  lcvexchlem4  39811  fipjust  44291  ntrkbimka  44764  ntrk0kbimka  44765  clsk3nimkb  44766  isotone2  44775  ntrclskb  44795  ntrclsk3  44796  ntrclsk13  44797  ismnushort  45011  relpfrlem  45662  permac8prim  45723  elrestd  45826  restsubel  45871  islptre  46335  islpcn  46353  subsaliuncllem  47071  subsaliuncl  47072  nnfoctbdjlem  47169  caragensplit  47214  vonvolmbllem  47374  vonvolmbl  47375  incsmflem  47455  decsmflem  47480  smflimlem2  47486  smflimlem3  47487  smflim  47491  smfpimcclem  47521  uzlidlring  49000  rngcvalALTV  49030  ringcvalALTV  49054  sepfsepc  49706  iscnrm3rlem2  49719  iscnrm3rlem8  49725  iscnrm3llem2  49728