Theorem ineq1 4213

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {crab 3436   ∩ cin 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958

This theorem is referenced by:  ineq2  4214  ineq12  4215  ineq1i  4216  ineq1d  4219  unineq  4288  dfrab3ss  4323  disjeq0  4456  inex1g  5319  reseq1  5991  sspred  6330  isofrlem  7360  qsdisj  8834  fiint  9366  fiintOLD  9367  elfiun  9470  dffi3  9471  inf3lema  9664  dfac5lem5  10167  kmlem12  10202  kmlem14  10204  fin23lem24  10362  fin23lem26  10365  fin23lem23  10366  fin23lem22  10367  fin23lem27  10368  ingru  10855  uzin2  15383  incexclem  15872  elrestr  17473  firest  17477  rngcval  20618  ringcval  20647  inopn  22905  isbasisg  22954  basis1  22957  basis2  22958  tgval  22962  fctop  23011  cctop  23013  ntrfval  23032  elcls  23081  clsndisj  23083  elcls3  23091  neindisj2  23131  tgrest  23167  restco  23172  restsn  23178  restcld  23180  restcldi  23181  restopnb  23183  neitr  23188  restcls  23189  ordtbaslem  23196  ordtrest2lem  23211  hausnei2  23361  cnhaus  23362  regsep2  23384  dishaus  23390  ordthauslem  23391  cmpsublem  23407  cmpsub  23408  nconnsubb  23431  connsubclo  23432  1stcelcls  23469  islly  23476  cldllycmp  23503  lly1stc  23504  locfincmp  23534  elkgen  23544  ptclsg  23623  dfac14lem  23625  txrest  23639  pthaus  23646  txhaus  23655  xkohaus  23661  xkoptsub  23662  regr1lem  23747  isfbas  23837  fbasssin  23844  fbun  23848  isfil  23855  fbunfip  23877  fgval  23878  filconn  23891  uzrest  23905  isufil2  23916  hauspwpwf1  23995  fclsopni  24023  fclsnei  24027  fclsrest  24032  fcfnei  24043  fcfneii  24045  tsmsfbas  24136  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  ust0  24228  trust  24238  restutopopn  24247  lpbl  24516  methaus  24533  metrest  24537  restmetu  24583  qtopbaslem  24779  qdensere  24790  xrtgioo  24828  metnrmlem3  24883  icoopnst  24969  iocopnst  24970  ovolicc2lem2  25553  ovolicc2lem5  25556  mblsplit  25567  limcnlp  25913  ellimc3  25914  limcflf  25916  limciun  25929  ig1pval  26215  shincl  31400  shmodi  31409  omlsi  31423  pjoml  31455  chm0  31510  chincl  31518  chdmm1  31544  ledi  31559  cmbr  31603  cmbr3  31627  mdbr  32313  dmdmd  32319  dmdi  32321  dmdbr3  32324  dmdbr4  32325  mdslmd1lem4  32347  cvmd  32355  cvexch  32393  dmdbr6ati  32442  mddmdin0i  32450  difeq  32537  ofpreima2  32676  ssdifidlprm  33486  ufdprmidl  33569  1arithufdlem4  33575  rspectopn  33866  ordtrest2NEWlem  33921  inelsros  34179  diffiunisros  34180  measvuni  34215  measinb  34222  inelcarsg  34313  carsgclctunlem2  34321  totprob  34429  ballotlemgval  34526  cvmscbv  35263  cvmsdisj  35275  cvmsss2  35279  satfv1  35368  nepss  35718  brapply  35939  opnbnd  36326  isfne  36340  tailfb  36378  bj-restsn  37083  bj-restpw  37093  bj-rest0  37094  bj-restb  37095  nlpfvineqsn  37410  fvineqsnf1  37411  pibt2  37418  ptrest  37626  poimirlem30  37657  mblfinlem2  37665  bndss  37793  qsdisjALTV  38616  redundss3  38629  lcvexchlem4  39038  fipjust  43578  ntrkbimka  44051  ntrk0kbimka  44052  clsk3nimkb  44053  isotone2  44062  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ismnushort  44320  relpfrlem  44974  elrestd  45113  restsubel  45158  islptre  45634  islpcn  45654  subsaliuncllem  46372  subsaliuncl  46373  nnfoctbdjlem  46470  caragensplit  46515  vonvolmbllem  46675  vonvolmbl  46676  incsmflem  46756  decsmflem  46781  smflimlem2  46787  smflimlem3  46788  smflim  46792  smfpimcclem  46822  uzlidlring  48151  rngcvalALTV  48181  ringcvalALTV  48205  sepfsepc  48825  iscnrm3rlem2  48838  iscnrm3rlem8  48844  iscnrm3llem2  48847