Theorem ineq1 4159

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3412   ∩ cin 3898

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  ineq2  4160  ineq12  4161  ineq1i  4162  ineq1d  4165  unineq  4234  dfrab3ss  4269  disjeq0  4409  inex1g  5282  reseq1  5966  sspred  6308  isofrlem  7342  qsdisj  8795  fiint  9297  elfiun  9401  dffi3  9402  inf3lema  9604  dfac5lem5  10131  kmlem12  10165  kmlem14  10167  fin23lem24  10325  fin23lem26  10328  fin23lem23  10329  fin23lem22  10330  fin23lem27  10331  ingru  10825  uzin2  15433  incexclem  15926  elrestr  17514  firest  17518  rngcval  20781  ringcval  20810  ssdifidlprm  21550  inopn  23125  isbasisg  23173  basis1  23176  basis2  23177  tgval  23181  fctop  23230  cctop  23232  ntrfval  23250  elcls  23299  clsndisj  23301  elcls3  23309  neindisj2  23349  tgrest  23385  restco  23390  restsn  23396  restcld  23398  restcldi  23399  restopnb  23401  neitr  23406  restcls  23407  ordtbaslem  23414  ordtrest2lem  23429  hausnei2  23579  cnhaus  23580  regsep2  23602  dishaus  23608  ordthauslem  23609  cmpsublem  23625  cmpsub  23626  nconnsubb  23649  connsubclo  23650  1stcelcls  23688  islly  23695  cldllycmp  23722  lly1stc  23723  locfincmp  23753  elkgen  23763  ptclsg  23842  dfac14lem  23844  txrest  23858  pthaus  23865  txhaus  23874  xkohaus  23880  xkoptsub  23881  regr1lem  23966  isfbas  24056  fbasssin  24063  fbun  24067  isfil  24074  fbunfip  24096  fgval  24097  filconn  24110  uzrest  24124  isufil2  24135  hauspwpwf1  24214  fclsopni  24242  fclsnei  24246  fclsrest  24251  fcfnei  24262  fcfneii  24264  tsmsfbas  24355  ustincl  24435  ustdiag  24436  ustinvel  24437  ustexhalf  24438  ust0  24447  trust  24456  restutopopn  24465  lpbl  24730  methaus  24747  metrest  24751  restmetu  24797  qtopbaslem  24985  qdensere  24996  xrtgioo  25034  metnrmlem3  25089  icoopnst  25168  iocopnst  25169  ovolicc2lem2  25747  ovolicc2lem5  25750  mblsplit  25761  limcnlp  26106  ellimc3  26107  limcflf  26109  limciun  26122  ig1pval  26402  shincl  31863  shmodi  31872  omlsi  31886  pjoml  31918  chm0  31973  chincl  31981  chdmm1  32007  ledi  32022  cmbr  32066  cmbr3  32090  mdbr  32776  dmdmd  32782  dmdi  32784  dmdbr3  32787  dmdbr4  32788  mdslmd1lem4  32810  cvmd  32818  cvexch  32856  dmdbr6ati  32905  mddmdin0i  32913  difeq  32994  ofpreima2  33140  ufdprmidl  33952  1arithufdlem4  33958  rspectopn  34378  ordtrest2NEWlem  34433  inelsros  34690  diffiunisros  34691  measvuni  34726  measinb  34733  inelcarsg  34823  carsgclctunlem2  34831  totprob  34939  ballotlemgval  35036  noinfepfnregs  35659  cvmscbv  35838  cvmsdisj  35850  cvmsss2  35854  satfv1  35943  nepss  36298  brapply  36516  opnbnd  36945  isfne  36959  tailfb  36997  dfttc4  37150  elttcirr  37151  bj-restsn  37833  bj-restpw  37843  bj-rest0  37844  bj-restb  37845  nlpfvineqsn  38164  fvineqsnf1  38165  pibt2  38172  ptrest  38369  poimirlem30  38400  mblfinlem2  38408  bndss  38537  qsdisjALTV  39448  redundss3  39461  lcvexchlem4  39911  fipjust  44406  ntrkbimka  44879  ntrk0kbimka  44880  clsk3nimkb  44881  isotone2  44890  ntrclskb  44910  ntrclsk3  44911  ntrclsk13  44912  ismnushort  45126  relpfrlem  45777  permac8prim  45838  elrestd  45941  restsubel  45986  islptre  46450  islpcn  46468  subsaliuncllem  47186  subsaliuncl  47187  nnfoctbdjlem  47284  caragensplit  47329  vonvolmbllem  47489  vonvolmbl  47490  incsmflem  47570  decsmflem  47595  smflimlem2  47601  smflimlem3  47602  smflim  47606  smfpimcclem  47636  uzlidlring  49151  rngcvalALTV  49181  ringcvalALTV  49205  sepfsepc  49855  iscnrm3rlem2  49868  iscnrm3rlem8  49874  iscnrm3llem2  49877