Theorem ineq1 4112

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  {crab 3415   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-in 4093

This theorem is used by:  ineq2  4113  ineq12  4114  ineq1i  4115  ineq1d  4118  unineq  4235  dfrab3ss  4270  disjeq0  4411  inex1g  5282  reseq1  5968  sspred  6319  isofrlem  7355  qsdisj  8826  fiint  9329  elfiun  9432  dffi3  9433  inf3lema  9635  dfac5lem5  10216  kmlem12  10250  kmlem14  10252  fin23lem24  10410  fin23lem26  10413  fin23lem23  10414  fin23lem22  10415  fin23lem27  10416  ingru  10910  uzin2  15524  incexclem  16017  elrestr  17611  firest  17615  rngcval  20882  ringcval  20911  ssdifidlprm  21654  inopn  23229  isbasisg  23277  basis1  23280  basis2  23281  tgval  23285  fctop  23334  cctop  23336  ntrfval  23354  elcls  23403  clsndisj  23405  elcls3  23413  neindisj2  23453  tgrest  23489  restco  23494  restsn  23500  restcld  23502  restcldi  23503  restopnb  23505  neitr  23510  restcls  23511  ordtbaslem  23518  ordtrest2lem  23533  hausnei2  23683  cnhaus  23684  regsep2  23706  dishaus  23712  ordthauslem  23713  cmpsublem  23729  cmpsub  23730  nconnsubb  23753  connsubclo  23754  1stcelcls  23792  islly  23799  cldllycmp  23826  lly1stc  23827  locfincmp  23857  elkgen  23867  ptclsg  23946  dfac14lem  23948  txrest  23962  pthaus  23969  txhaus  23978  xkohaus  23984  xkoptsub  23985  regr1lem  24070  isfbas  24160  fbasssin  24167  fbun  24171  isfil  24178  fbunfip  24200  fgval  24201  filconn  24214  uzrest  24228  isufil2  24239  hauspwpwf1  24318  fclsopni  24346  fclsnei  24350  fclsrest  24355  fcfnei  24366  fcfneii  24368  tsmsfbas  24459  ustincl  24539  ustdiag  24540  ustinvel  24541  ustexhalf  24542  ust0  24551  trust  24560  restutopopn  24569  lpbl  24834  methaus  24851  metrest  24855  restmetu  24901  qtopbaslem  25089  qdensere  25100  xrtgioo  25138  metnrmlem3  25193  icoopnst  25272  iocopnst  25273  ovolicc2lem2  25851  ovolicc2lem5  25854  mblsplit  25865  limcnlp  26210  ellimc3  26211  limcflf  26213  limciun  26226  ig1pval  26506  shincl  31995  shmodi  32004  omlsi  32018  pjoml  32050  chm0  32105  chincl  32113  chdmm1  32139  ledi  32154  cmbr  32198  cmbr3  32222  mdbr  32908  dmdmd  32914  dmdi  32916  dmdbr3  32919  dmdbr4  32920  mdslmd1lem4  32942  cvmd  32950  cvexch  32988  dmdbr6ati  33037  mddmdin0i  33045  difeq  33168  ofpreima2  33314  ufdprmidl  34126  1arithufdlem4  34132  rspectopn  34552  ordtrest2NEWlem  34607  inelsros  34864  diffiunisros  34865  measvuni  34900  measinb  34907  inelcarsg  34996  carsgclctunlem2  35004  totprob  35112  ballotlemgval  35209  noinfepfnregs  35871  cvmscbv  36144  cvmsdisj  36156  cvmsss2  36160  satfv1  36249  nepss  36610  brapply  36827  opnbnd  37240  isfne  37254  tailfb  37292  dfttc4  37445  elttcirr  37446  bj-restsn  38142  bj-restpw  38152  bj-rest0  38153  bj-restb  38154  nlpfvineqsn  38472  fvineqsnf1  38473  pibt2  38480  ptrest  38677  poimirlem30  38708  mblfinlem2  38716  bndss  38860  qsdisjALTV  39771  redundss3  39784  lcvexchlem4  40234  fipjust  44706  ntrkbimka  45178  ntrk0kbimka  45179  clsk3nimkb  45180  isotone2  45189  ntrclskb  45209  ntrclsk3  45210  ntrclsk13  45211  ismnushort  45425  relpfrlem  46082  permac8prim  46143  elrestd  46262  restsubel  46307  islptre  46770  islpcn  46788  subsaliuncllem  47506  subsaliuncl  47507  nnfoctbdjlem  47604  caragensplit  47649  vonvolmbllem  47809  vonvolmbl  47810  incsmflem  47890  decsmflem  47915  smflimlem2  47921  smflimlem3  47922  smflim  47926  smfpimcclem  47956  uzlidlring  49471  rngcvalALTV  49501  ringcvalALTV  49525  sepfsepc  50181  iscnrm3rlem2  50194  iscnrm3rlem8  50200  iscnrm3llem2  50203