Theorem ineq1 4154

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897

This theorem is referenced by:  ineq2  4155  ineq12  4156  ineq1i  4157  ineq1d  4160  unineq  4229  dfrab3ss  4264  disjeq0  4397  inex1g  5257  reseq1  5933  sspred  6269  isofrlem  7289  qsdisj  8735  fiint  9231  elfiun  9337  dffi3  9338  inf3lema  9539  dfac5lem5  10043  kmlem12  10078  kmlem14  10080  fin23lem24  10238  fin23lem26  10241  fin23lem23  10242  fin23lem22  10243  fin23lem27  10244  ingru  10732  uzin2  15301  incexclem  15795  elrestr  17385  firest  17389  rngcval  20589  ringcval  20618  inopn  22877  isbasisg  22925  basis1  22928  basis2  22929  tgval  22933  fctop  22982  cctop  22984  ntrfval  23002  elcls  23051  clsndisj  23053  elcls3  23061  neindisj2  23101  tgrest  23137  restco  23142  restsn  23148  restcld  23150  restcldi  23151  restopnb  23153  neitr  23158  restcls  23159  ordtbaslem  23166  ordtrest2lem  23181  hausnei2  23331  cnhaus  23332  regsep2  23354  dishaus  23360  ordthauslem  23361  cmpsublem  23377  cmpsub  23378  nconnsubb  23401  connsubclo  23402  1stcelcls  23439  islly  23446  cldllycmp  23473  lly1stc  23474  locfincmp  23504  elkgen  23514  ptclsg  23593  dfac14lem  23595  txrest  23609  pthaus  23616  txhaus  23625  xkohaus  23631  xkoptsub  23632  regr1lem  23717  isfbas  23807  fbasssin  23814  fbun  23818  isfil  23825  fbunfip  23847  fgval  23848  filconn  23861  uzrest  23875  isufil2  23886  hauspwpwf1  23965  fclsopni  23993  fclsnei  23997  fclsrest  24002  fcfnei  24013  fcfneii  24015  tsmsfbas  24106  ustincl  24186  ustdiag  24187  ustinvel  24188  ustexhalf  24189  ust0  24198  trust  24207  restutopopn  24216  lpbl  24481  methaus  24498  metrest  24502  restmetu  24548  qtopbaslem  24736  qdensere  24747  xrtgioo  24785  metnrmlem3  24840  icoopnst  24919  iocopnst  24920  ovolicc2lem2  25498  ovolicc2lem5  25501  mblsplit  25512  limcnlp  25858  ellimc3  25859  limcflf  25861  limciun  25874  ig1pval  26154  shincl  31470  shmodi  31479  omlsi  31493  pjoml  31525  chm0  31580  chincl  31588  chdmm1  31614  ledi  31629  cmbr  31673  cmbr3  31697  mdbr  32383  dmdmd  32389  dmdi  32391  dmdbr3  32394  dmdbr4  32395  mdslmd1lem4  32417  cvmd  32425  cvexch  32463  dmdbr6ati  32512  mddmdin0i  32520  difeq  32606  ofpreima2  32757  ssdifidlprm  33536  ufdprmidl  33619  1arithufdlem4  33625  rspectopn  34030  ordtrest2NEWlem  34085  inelsros  34341  diffiunisros  34342  measvuni  34377  measinb  34384  inelcarsg  34474  carsgclctunlem2  34482  totprob  34590  ballotlemgval  34687  noinfepfnregs  35295  cvmscbv  35459  cvmsdisj  35471  cvmsss2  35475  satfv1  35564  nepss  35919  brapply  36137  opnbnd  36526  isfne  36540  tailfb  36578  dfttc4  36731  elttcirr  36732  bj-restsn  37413  bj-restpw  37423  bj-rest0  37424  bj-restb  37425  nlpfvineqsn  37742  fvineqsnf1  37743  pibt2  37750  ptrest  37957  poimirlem30  37988  mblfinlem2  37996  bndss  38124  qsdisjALTV  39037  redundss3  39050  lcvexchlem4  39500  fipjust  44013  ntrkbimka  44486  ntrk0kbimka  44487  clsk3nimkb  44488  isotone2  44497  ntrclskb  44517  ntrclsk3  44518  ntrclsk13  44519  ismnushort  44749  relpfrlem  45401  permac8prim  45462  elrestd  45559  restsubel  45604  islptre  46070  islpcn  46088  subsaliuncllem  46806  subsaliuncl  46807  nnfoctbdjlem  46904  caragensplit  46949  vonvolmbllem  47109  vonvolmbl  47110  incsmflem  47190  decsmflem  47215  smflimlem2  47221  smflimlem3  47222  smflim  47226  smfpimcclem  47256  uzlidlring  48726  rngcvalALTV  48756  ringcvalALTV  48780  sepfsepc  49418  iscnrm3rlem2  49431  iscnrm3rlem8  49437  iscnrm3llem2  49440