Theorem ineq1 4172

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3402   ∩ cin 3910

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918

This theorem is referenced by:  ineq2  4173  ineq12  4174  ineq1i  4175  ineq1d  4178  unineq  4247  dfrab3ss  4282  disjeq0  4415  inex1g  5269  reseq1  5933  sspred  6271  isofrlem  7297  qsdisj  8744  fiint  9253  fiintOLD  9254  elfiun  9357  dffi3  9358  inf3lema  9553  dfac5lem5  10056  kmlem12  10091  kmlem14  10093  fin23lem24  10251  fin23lem26  10254  fin23lem23  10255  fin23lem22  10256  fin23lem27  10257  ingru  10744  uzin2  15287  incexclem  15778  elrestr  17367  firest  17371  rngcval  20538  ringcval  20567  inopn  22819  isbasisg  22867  basis1  22870  basis2  22871  tgval  22875  fctop  22924  cctop  22926  ntrfval  22944  elcls  22993  clsndisj  22995  elcls3  23003  neindisj2  23043  tgrest  23079  restco  23084  restsn  23090  restcld  23092  restcldi  23093  restopnb  23095  neitr  23100  restcls  23101  ordtbaslem  23108  ordtrest2lem  23123  hausnei2  23273  cnhaus  23274  regsep2  23296  dishaus  23302  ordthauslem  23303  cmpsublem  23319  cmpsub  23320  nconnsubb  23343  connsubclo  23344  1stcelcls  23381  islly  23388  cldllycmp  23415  lly1stc  23416  locfincmp  23446  elkgen  23456  ptclsg  23535  dfac14lem  23537  txrest  23551  pthaus  23558  txhaus  23567  xkohaus  23573  xkoptsub  23574  regr1lem  23659  isfbas  23749  fbasssin  23756  fbun  23760  isfil  23767  fbunfip  23789  fgval  23790  filconn  23803  uzrest  23817  isufil2  23828  hauspwpwf1  23907  fclsopni  23935  fclsnei  23939  fclsrest  23944  fcfnei  23955  fcfneii  23957  tsmsfbas  24048  ustincl  24128  ustdiag  24129  ustinvel  24130  ustexhalf  24131  ust0  24140  trust  24150  restutopopn  24159  lpbl  24424  methaus  24441  metrest  24445  restmetu  24491  qtopbaslem  24679  qdensere  24690  xrtgioo  24728  metnrmlem3  24783  icoopnst  24869  iocopnst  24870  ovolicc2lem2  25452  ovolicc2lem5  25455  mblsplit  25466  limcnlp  25812  ellimc3  25813  limcflf  25815  limciun  25828  ig1pval  26114  shincl  31360  shmodi  31369  omlsi  31383  pjoml  31415  chm0  31470  chincl  31478  chdmm1  31504  ledi  31519  cmbr  31563  cmbr3  31587  mdbr  32273  dmdmd  32279  dmdi  32281  dmdbr3  32284  dmdbr4  32285  mdslmd1lem4  32307  cvmd  32315  cvexch  32353  dmdbr6ati  32402  mddmdin0i  32410  difeq  32497  ofpreima2  32640  ssdifidlprm  33422  ufdprmidl  33505  1arithufdlem4  33511  rspectopn  33850  ordtrest2NEWlem  33905  inelsros  34161  diffiunisros  34162  measvuni  34197  measinb  34204  inelcarsg  34295  carsgclctunlem2  34303  totprob  34411  ballotlemgval  34508  cvmscbv  35238  cvmsdisj  35250  cvmsss2  35254  satfv1  35343  nepss  35698  brapply  35919  opnbnd  36306  isfne  36320  tailfb  36358  bj-restsn  37063  bj-restpw  37073  bj-rest0  37074  bj-restb  37075  nlpfvineqsn  37390  fvineqsnf1  37391  pibt2  37398  ptrest  37606  poimirlem30  37637  mblfinlem2  37645  bndss  37773  qsdisjALTV  38599  redundss3  38612  lcvexchlem4  39023  fipjust  43547  ntrkbimka  44020  ntrk0kbimka  44021  clsk3nimkb  44022  isotone2  44031  ntrclskb  44051  ntrclsk3  44052  ntrclsk13  44053  ismnushort  44283  relpfrlem  44936  permac8prim  44997  elrestd  45095  restsubel  45140  islptre  45610  islpcn  45630  subsaliuncllem  46348  subsaliuncl  46349  nnfoctbdjlem  46446  caragensplit  46491  vonvolmbllem  46651  vonvolmbl  46652  incsmflem  46732  decsmflem  46757  smflimlem2  46763  smflimlem3  46764  smflim  46768  smfpimcclem  46798  uzlidlring  48216  rngcvalALTV  48246  ringcvalALTV  48270  sepfsepc  48909  iscnrm3rlem2  48922  iscnrm3rlem8  48928  iscnrm3llem2  48931