Theorem ineq1 4220

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  {crab 3432   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969

This theorem is referenced by:  ineq2  4221  ineq12  4222  ineq1i  4223  ineq1d  4226  unineq  4293  dfrab3ss  4328  disjeq0  4461  inex1g  5324  reseq1  5993  sspred  6331  isofrlem  7359  qsdisj  8832  fiint  9363  fiintOLD  9364  elfiun  9467  dffi3  9468  inf3lema  9661  dfac5lem5  10164  kmlem12  10199  kmlem14  10201  fin23lem24  10359  fin23lem26  10362  fin23lem23  10363  fin23lem22  10364  fin23lem27  10365  ingru  10852  uzin2  15379  incexclem  15868  elrestr  17474  firest  17478  rngcval  20634  ringcval  20663  inopn  22920  isbasisg  22969  basis1  22972  basis2  22973  tgval  22977  fctop  23026  cctop  23028  ntrfval  23047  elcls  23096  clsndisj  23098  elcls3  23106  neindisj2  23146  tgrest  23182  restco  23187  restsn  23193  restcld  23195  restcldi  23196  restopnb  23198  neitr  23203  restcls  23204  ordtbaslem  23211  ordtrest2lem  23226  hausnei2  23376  cnhaus  23377  regsep2  23399  dishaus  23405  ordthauslem  23406  cmpsublem  23422  cmpsub  23423  nconnsubb  23446  connsubclo  23447  1stcelcls  23484  islly  23491  cldllycmp  23518  lly1stc  23519  locfincmp  23549  elkgen  23559  ptclsg  23638  dfac14lem  23640  txrest  23654  pthaus  23661  txhaus  23670  xkohaus  23676  xkoptsub  23677  regr1lem  23762  isfbas  23852  fbasssin  23859  fbun  23863  isfil  23870  fbunfip  23892  fgval  23893  filconn  23906  uzrest  23920  isufil2  23931  hauspwpwf1  24010  fclsopni  24038  fclsnei  24042  fclsrest  24047  fcfnei  24058  fcfneii  24060  tsmsfbas  24151  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  ust0  24243  trust  24253  restutopopn  24262  lpbl  24531  methaus  24548  metrest  24552  restmetu  24598  qtopbaslem  24794  qdensere  24805  xrtgioo  24841  metnrmlem3  24896  icoopnst  24982  iocopnst  24983  ovolicc2lem2  25566  ovolicc2lem5  25569  mblsplit  25580  limcnlp  25927  ellimc3  25928  limcflf  25930  limciun  25943  ig1pval  26229  shincl  31409  shmodi  31418  omlsi  31432  pjoml  31464  chm0  31519  chincl  31527  chdmm1  31553  ledi  31568  cmbr  31612  cmbr3  31636  mdbr  32322  dmdmd  32328  dmdi  32330  dmdbr3  32333  dmdbr4  32334  mdslmd1lem4  32356  cvmd  32364  cvexch  32402  dmdbr6ati  32451  mddmdin0i  32459  difeq  32545  ofpreima2  32682  ssdifidlprm  33465  ufdprmidl  33548  1arithufdlem4  33554  rspectopn  33827  ordtrest2NEWlem  33882  inelsros  34158  diffiunisros  34159  measvuni  34194  measinb  34201  inelcarsg  34292  carsgclctunlem2  34300  totprob  34408  ballotlemgval  34504  cvmscbv  35242  cvmsdisj  35254  cvmsss2  35258  satfv1  35347  nepss  35697  brapply  35919  opnbnd  36307  isfne  36321  tailfb  36359  bj-restsn  37064  bj-restpw  37074  bj-rest0  37075  bj-restb  37076  nlpfvineqsn  37391  fvineqsnf1  37392  pibt2  37399  ptrest  37605  poimirlem30  37636  mblfinlem2  37644  bndss  37772  qsdisjALTV  38596  redundss3  38609  lcvexchlem4  39018  fipjust  43554  ntrkbimka  44027  ntrk0kbimka  44028  clsk3nimkb  44029  isotone2  44038  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ismnushort  44296  elrestd  45047  restsubel  45095  islptre  45574  islpcn  45594  subsaliuncllem  46312  subsaliuncl  46313  nnfoctbdjlem  46410  caragensplit  46455  vonvolmbllem  46615  vonvolmbl  46616  incsmflem  46696  decsmflem  46721  smflimlem2  46727  smflimlem3  46728  smflim  46732  smfpimcclem  46762  uzlidlring  48078  rngcvalALTV  48108  ringcvalALTV  48132  sepfsepc  48723  iscnrm3rlem2  48737  iscnrm3rlem8  48743  iscnrm3llem2  48746