Theorem ineq1 4153

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3389   ∩ cin 3888

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  ineq2  4154  ineq12  4155  ineq1i  4156  ineq1d  4159  unineq  4228  dfrab3ss  4263  disjeq0  4396  inex1g  5260  reseq1  5938  sspred  6274  isofrlem  7295  qsdisj  8741  fiint  9237  elfiun  9343  dffi3  9344  inf3lema  9545  dfac5lem5  10049  kmlem12  10084  kmlem14  10086  fin23lem24  10244  fin23lem26  10247  fin23lem23  10248  fin23lem22  10249  fin23lem27  10250  ingru  10738  uzin2  15307  incexclem  15801  elrestr  17391  firest  17395  rngcval  20595  ringcval  20624  inopn  22864  isbasisg  22912  basis1  22915  basis2  22916  tgval  22920  fctop  22969  cctop  22971  ntrfval  22989  elcls  23038  clsndisj  23040  elcls3  23048  neindisj2  23088  tgrest  23124  restco  23129  restsn  23135  restcld  23137  restcldi  23138  restopnb  23140  neitr  23145  restcls  23146  ordtbaslem  23153  ordtrest2lem  23168  hausnei2  23318  cnhaus  23319  regsep2  23341  dishaus  23347  ordthauslem  23348  cmpsublem  23364  cmpsub  23365  nconnsubb  23388  connsubclo  23389  1stcelcls  23426  islly  23433  cldllycmp  23460  lly1stc  23461  locfincmp  23491  elkgen  23501  ptclsg  23580  dfac14lem  23582  txrest  23596  pthaus  23603  txhaus  23612  xkohaus  23618  xkoptsub  23619  regr1lem  23704  isfbas  23794  fbasssin  23801  fbun  23805  isfil  23812  fbunfip  23834  fgval  23835  filconn  23848  uzrest  23862  isufil2  23873  hauspwpwf1  23952  fclsopni  23980  fclsnei  23984  fclsrest  23989  fcfnei  24000  fcfneii  24002  tsmsfbas  24093  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ust0  24185  trust  24194  restutopopn  24203  lpbl  24468  methaus  24485  metrest  24489  restmetu  24535  qtopbaslem  24723  qdensere  24734  xrtgioo  24772  metnrmlem3  24827  icoopnst  24906  iocopnst  24907  ovolicc2lem2  25485  ovolicc2lem5  25488  mblsplit  25499  limcnlp  25845  ellimc3  25846  limcflf  25848  limciun  25861  ig1pval  26141  shincl  31452  shmodi  31461  omlsi  31475  pjoml  31507  chm0  31562  chincl  31570  chdmm1  31596  ledi  31611  cmbr  31655  cmbr3  31679  mdbr  32365  dmdmd  32371  dmdi  32373  dmdbr3  32376  dmdbr4  32377  mdslmd1lem4  32399  cvmd  32407  cvexch  32445  dmdbr6ati  32494  mddmdin0i  32502  difeq  32588  ofpreima2  32739  ssdifidlprm  33518  ufdprmidl  33601  1arithufdlem4  33607  rspectopn  34011  ordtrest2NEWlem  34066  inelsros  34322  diffiunisros  34323  measvuni  34358  measinb  34365  inelcarsg  34455  carsgclctunlem2  34463  totprob  34571  ballotlemgval  34668  noinfepfnregs  35276  cvmscbv  35440  cvmsdisj  35452  cvmsss2  35456  satfv1  35545  nepss  35900  brapply  36118  opnbnd  36507  isfne  36521  tailfb  36559  dfttc4  36712  elttcirr  36713  bj-restsn  37394  bj-restpw  37404  bj-rest0  37405  bj-restb  37406  nlpfvineqsn  37725  fvineqsnf1  37726  pibt2  37733  ptrest  37940  poimirlem30  37971  mblfinlem2  37979  bndss  38107  qsdisjALTV  39020  redundss3  39033  lcvexchlem4  39483  fipjust  43992  ntrkbimka  44465  ntrk0kbimka  44466  clsk3nimkb  44467  isotone2  44476  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ismnushort  44728  relpfrlem  45380  permac8prim  45441  elrestd  45538  restsubel  45583  islptre  46049  islpcn  46067  subsaliuncllem  46785  subsaliuncl  46786  nnfoctbdjlem  46883  caragensplit  46928  vonvolmbllem  47088  vonvolmbl  47089  incsmflem  47169  decsmflem  47194  smflimlem2  47200  smflimlem3  47201  smflim  47205  smfpimcclem  47235  uzlidlring  48711  rngcvalALTV  48741  ringcvalALTV  48765  sepfsepc  49403  iscnrm3rlem2  49416  iscnrm3rlem8  49422  iscnrm3llem2  49425