Theorem ineq1 4163

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3397   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-in 3906

This theorem is referenced by:  ineq2  4164  ineq12  4165  ineq1i  4166  ineq1d  4169  unineq  4238  dfrab3ss  4273  disjeq0  4406  inex1g  5262  reseq1  5930  sspred  6266  isofrlem  7284  qsdisj  8729  fiint  9225  elfiun  9331  dffi3  9332  inf3lema  9531  dfac5lem5  10035  kmlem12  10070  kmlem14  10072  fin23lem24  10230  fin23lem26  10233  fin23lem23  10234  fin23lem22  10235  fin23lem27  10236  ingru  10724  uzin2  15266  incexclem  15757  elrestr  17346  firest  17350  rngcval  20549  ringcval  20578  inopn  22841  isbasisg  22889  basis1  22892  basis2  22893  tgval  22897  fctop  22946  cctop  22948  ntrfval  22966  elcls  23015  clsndisj  23017  elcls3  23025  neindisj2  23065  tgrest  23101  restco  23106  restsn  23112  restcld  23114  restcldi  23115  restopnb  23117  neitr  23122  restcls  23123  ordtbaslem  23130  ordtrest2lem  23145  hausnei2  23295  cnhaus  23296  regsep2  23318  dishaus  23324  ordthauslem  23325  cmpsublem  23341  cmpsub  23342  nconnsubb  23365  connsubclo  23366  1stcelcls  23403  islly  23410  cldllycmp  23437  lly1stc  23438  locfincmp  23468  elkgen  23478  ptclsg  23557  dfac14lem  23559  txrest  23573  pthaus  23580  txhaus  23589  xkohaus  23595  xkoptsub  23596  regr1lem  23681  isfbas  23771  fbasssin  23778  fbun  23782  isfil  23789  fbunfip  23811  fgval  23812  filconn  23825  uzrest  23839  isufil2  23850  hauspwpwf1  23929  fclsopni  23957  fclsnei  23961  fclsrest  23966  fcfnei  23977  fcfneii  23979  tsmsfbas  24070  ustincl  24150  ustdiag  24151  ustinvel  24152  ustexhalf  24153  ust0  24162  trust  24171  restutopopn  24180  lpbl  24445  methaus  24462  metrest  24466  restmetu  24512  qtopbaslem  24700  qdensere  24711  xrtgioo  24749  metnrmlem3  24804  icoopnst  24890  iocopnst  24891  ovolicc2lem2  25473  ovolicc2lem5  25476  mblsplit  25487  limcnlp  25833  ellimc3  25834  limcflf  25836  limciun  25849  ig1pval  26135  shincl  31405  shmodi  31414  omlsi  31428  pjoml  31460  chm0  31515  chincl  31523  chdmm1  31549  ledi  31564  cmbr  31608  cmbr3  31632  mdbr  32318  dmdmd  32324  dmdi  32326  dmdbr3  32329  dmdbr4  32330  mdslmd1lem4  32352  cvmd  32360  cvexch  32398  dmdbr6ati  32447  mddmdin0i  32455  difeq  32542  ofpreima2  32693  ssdifidlprm  33488  ufdprmidl  33571  1arithufdlem4  33577  rspectopn  33973  ordtrest2NEWlem  34028  inelsros  34284  diffiunisros  34285  measvuni  34320  measinb  34327  inelcarsg  34417  carsgclctunlem2  34425  totprob  34533  ballotlemgval  34630  noinfepfnregs  35237  cvmscbv  35401  cvmsdisj  35413  cvmsss2  35417  satfv1  35506  nepss  35861  brapply  36079  opnbnd  36468  isfne  36482  tailfb  36520  bj-restsn  37226  bj-restpw  37236  bj-rest0  37237  bj-restb  37238  nlpfvineqsn  37553  fvineqsnf1  37554  pibt2  37561  ptrest  37759  poimirlem30  37790  mblfinlem2  37798  bndss  37926  qsdisjALTV  38811  redundss3  38824  lcvexchlem4  39236  fipjust  43748  ntrkbimka  44221  ntrk0kbimka  44222  clsk3nimkb  44223  isotone2  44232  ntrclskb  44252  ntrclsk3  44253  ntrclsk13  44254  ismnushort  44484  relpfrlem  45136  permac8prim  45197  elrestd  45294  restsubel  45339  islptre  45807  islpcn  45825  subsaliuncllem  46543  subsaliuncl  46544  nnfoctbdjlem  46641  caragensplit  46686  vonvolmbllem  46846  vonvolmbl  46847  incsmflem  46927  decsmflem  46952  smflimlem2  46958  smflimlem3  46959  smflim  46963  smfpimcclem  46993  uzlidlring  48423  rngcvalALTV  48453  ringcvalALTV  48477  sepfsepc  49115  iscnrm3rlem2  49128  iscnrm3rlem8  49134  iscnrm3llem2  49137