Theorem ineq1 4174

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {crab 3423   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  ineq2  4175  ineq12  4176  ineq1i  4177  ineq1d  4180  unineq  4249  dfrab3ss  4284  disjeq0  4422  inex1g  5290  reseq1  5973  sspred  6312  isofrlem  7339  qsdisj  8791  fiint  9285  elfiun  9389  dffi3  9390  inf3lema  9592  dfac5lem5  10110  kmlem12  10144  kmlem14  10146  fin23lem24  10305  fin23lem26  10308  fin23lem23  10309  fin23lem22  10310  fin23lem27  10311  ingru  10799  uzin2  15395  incexclem  15889  elrestr  17480  firest  17484  rngcval  20702  ringcval  20731  ssdifidlprm  21454  inopn  23024  isbasisg  23072  basis1  23075  basis2  23076  tgval  23080  fctop  23129  cctop  23131  ntrfval  23149  elcls  23198  clsndisj  23200  elcls3  23208  neindisj2  23248  tgrest  23284  restco  23289  restsn  23295  restcld  23297  restcldi  23298  restopnb  23300  neitr  23305  restcls  23306  ordtbaslem  23313  ordtrest2lem  23328  hausnei2  23478  cnhaus  23479  regsep2  23501  dishaus  23507  ordthauslem  23508  cmpsublem  23524  cmpsub  23525  nconnsubb  23548  connsubclo  23549  1stcelcls  23586  islly  23593  cldllycmp  23620  lly1stc  23621  locfincmp  23651  elkgen  23661  ptclsg  23740  dfac14lem  23742  txrest  23756  pthaus  23763  txhaus  23772  xkohaus  23778  xkoptsub  23779  regr1lem  23864  isfbas  23954  fbasssin  23961  fbun  23965  isfil  23972  fbunfip  23994  fgval  23995  filconn  24008  uzrest  24022  isufil2  24033  hauspwpwf1  24112  fclsopni  24140  fclsnei  24144  fclsrest  24149  fcfnei  24160  fcfneii  24162  tsmsfbas  24253  ustincl  24333  ustdiag  24334  ustinvel  24335  ustexhalf  24336  ust0  24345  trust  24354  restutopopn  24363  lpbl  24628  methaus  24645  metrest  24649  restmetu  24695  qtopbaslem  24883  qdensere  24894  xrtgioo  24932  metnrmlem3  24987  icoopnst  25066  iocopnst  25067  ovolicc2lem2  25645  ovolicc2lem5  25648  mblsplit  25659  limcnlp  26005  ellimc3  26006  limcflf  26008  limciun  26021  ig1pval  26301  shincl  31673  shmodi  31682  omlsi  31696  pjoml  31728  chm0  31783  chincl  31791  chdmm1  31817  ledi  31832  cmbr  31876  cmbr3  31900  mdbr  32586  dmdmd  32592  dmdi  32594  dmdbr3  32597  dmdbr4  32598  mdslmd1lem4  32620  cvmd  32628  cvexch  32666  dmdbr6ati  32715  mddmdin0i  32723  difeq  32804  ofpreima2  32951  ufdprmidl  33775  1arithufdlem4  33781  rspectopn  34201  ordtrest2NEWlem  34256  inelsros  34512  diffiunisros  34513  measvuni  34548  measinb  34555  inelcarsg  34645  carsgclctunlem2  34653  totprob  34761  ballotlemgval  34858  noinfepfnregs  35467  cvmscbv  35648  cvmsdisj  35660  cvmsss2  35664  satfv1  35753  nepss  36108  brapply  36326  opnbnd  36724  isfne  36738  tailfb  36776  dfttc4  36929  elttcirr  36930  bj-restsn  37611  bj-restpw  37621  bj-rest0  37622  bj-restb  37623  nlpfvineqsn  37942  fvineqsnf1  37943  pibt2  37950  ptrest  38157  poimirlem30  38188  mblfinlem2  38196  bndss  38324  qsdisjALTV  39237  redundss3  39250  lcvexchlem4  39700  fipjust  44182  ntrkbimka  44655  ntrk0kbimka  44656  clsk3nimkb  44657  isotone2  44666  ntrclskb  44686  ntrclsk3  44687  ntrclsk13  44688  ismnushort  44902  relpfrlem  45553  permac8prim  45614  elrestd  45717  restsubel  45762  islptre  46226  islpcn  46244  subsaliuncllem  46962  subsaliuncl  46963  nnfoctbdjlem  47060  caragensplit  47105  vonvolmbllem  47265  vonvolmbl  47266  incsmflem  47346  decsmflem  47371  smflimlem2  47377  smflimlem3  47378  smflim  47382  smfpimcclem  47412  uzlidlring  48888  rngcvalALTV  48918  ringcvalALTV  48942  sepfsepc  49590  iscnrm3rlem2  49603  iscnrm3rlem8  49609  iscnrm3llem2  49612