Theorem ineq1 4166

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  {crab 3418   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  ineq2  4167  ineq12  4168  ineq1i  4169  ineq1d  4172  unineq  4241  dfrab3ss  4276  disjeq0  4416  inex1g  5290  reseq1  5974  sspred  6315  isofrlem  7347  qsdisj  8798  fiint  9293  elfiun  9397  dffi3  9398  inf3lema  9600  dfac5lem5  10127  kmlem12  10161  kmlem14  10163  fin23lem24  10321  fin23lem26  10324  fin23lem23  10325  fin23lem22  10326  fin23lem27  10327  ingru  10815  uzin2  15420  incexclem  15913  elrestr  17503  firest  17507  rngcval  20767  ringcval  20796  ssdifidlprm  21536  inopn  23106  isbasisg  23154  basis1  23157  basis2  23158  tgval  23162  fctop  23211  cctop  23213  ntrfval  23231  elcls  23280  clsndisj  23282  elcls3  23290  neindisj2  23330  tgrest  23366  restco  23371  restsn  23377  restcld  23379  restcldi  23380  restopnb  23382  neitr  23387  restcls  23388  ordtbaslem  23395  ordtrest2lem  23410  hausnei2  23560  cnhaus  23561  regsep2  23583  dishaus  23589  ordthauslem  23590  cmpsublem  23606  cmpsub  23607  nconnsubb  23630  connsubclo  23631  1stcelcls  23669  islly  23676  cldllycmp  23703  lly1stc  23704  locfincmp  23734  elkgen  23744  ptclsg  23823  dfac14lem  23825  txrest  23839  pthaus  23846  txhaus  23855  xkohaus  23861  xkoptsub  23862  regr1lem  23947  isfbas  24037  fbasssin  24044  fbun  24048  isfil  24055  fbunfip  24077  fgval  24078  filconn  24091  uzrest  24105  isufil2  24116  hauspwpwf1  24195  fclsopni  24223  fclsnei  24227  fclsrest  24232  fcfnei  24243  fcfneii  24245  tsmsfbas  24336  ustincl  24416  ustdiag  24417  ustinvel  24418  ustexhalf  24419  ust0  24428  trust  24437  restutopopn  24446  lpbl  24711  methaus  24728  metrest  24732  restmetu  24778  qtopbaslem  24966  qdensere  24977  xrtgioo  25015  metnrmlem3  25070  icoopnst  25149  iocopnst  25150  ovolicc2lem2  25728  ovolicc2lem5  25731  mblsplit  25742  limcnlp  26088  ellimc3  26089  limcflf  26091  limciun  26104  ig1pval  26384  shincl  31804  shmodi  31813  omlsi  31827  pjoml  31859  chm0  31914  chincl  31922  chdmm1  31948  ledi  31963  cmbr  32007  cmbr3  32031  mdbr  32717  dmdmd  32723  dmdi  32725  dmdbr3  32728  dmdbr4  32729  mdslmd1lem4  32751  cvmd  32759  cvexch  32797  dmdbr6ati  32846  mddmdin0i  32854  difeq  32935  ofpreima2  33082  ufdprmidl  33895  1arithufdlem4  33901  rspectopn  34321  ordtrest2NEWlem  34376  inelsros  34633  diffiunisros  34634  measvuni  34669  measinb  34676  inelcarsg  34766  carsgclctunlem2  34774  totprob  34882  ballotlemgval  34979  noinfepfnregs  35602  cvmscbv  35787  cvmsdisj  35799  cvmsss2  35803  satfv1  35892  nepss  36247  brapply  36465  opnbnd  36893  isfne  36907  tailfb  36945  dfttc4  37098  elttcirr  37099  bj-restsn  37781  bj-restpw  37791  bj-rest0  37792  bj-restb  37793  nlpfvineqsn  38112  fvineqsnf1  38113  pibt2  38120  ptrest  38327  poimirlem30  38358  mblfinlem2  38366  bndss  38495  qsdisjALTV  39406  redundss3  39419  lcvexchlem4  39869  fipjust  44349  ntrkbimka  44822  ntrk0kbimka  44823  clsk3nimkb  44824  isotone2  44833  ntrclskb  44853  ntrclsk3  44854  ntrclsk13  44855  ismnushort  45069  relpfrlem  45720  permac8prim  45781  elrestd  45884  restsubel  45929  islptre  46393  islpcn  46411  subsaliuncllem  47129  subsaliuncl  47130  nnfoctbdjlem  47227  caragensplit  47272  vonvolmbllem  47432  vonvolmbl  47433  incsmflem  47513  decsmflem  47538  smflimlem2  47544  smflimlem3  47545  smflim  47549  smfpimcclem  47579  uzlidlring  49057  rngcvalALTV  49087  ringcvalALTV  49111  sepfsepc  49763  iscnrm3rlem2  49776  iscnrm3rlem8  49782  iscnrm3llem2  49785