Theorem ineq1 4176

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

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

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 3406  df-in 3921

This theorem is referenced by:  ineq2  4177  ineq12  4178  ineq1i  4179  ineq1d  4182  unineq  4251  dfrab3ss  4286  disjeq0  4419  inex1g  5274  reseq1  5944  sspred  6283  isofrlem  7315  qsdisj  8767  fiint  9277  fiintOLD  9278  elfiun  9381  dffi3  9382  inf3lema  9577  dfac5lem5  10080  kmlem12  10115  kmlem14  10117  fin23lem24  10275  fin23lem26  10278  fin23lem23  10279  fin23lem22  10280  fin23lem27  10281  ingru  10768  uzin2  15311  incexclem  15802  elrestr  17391  firest  17395  rngcval  20527  ringcval  20556  inopn  22786  isbasisg  22834  basis1  22837  basis2  22838  tgval  22842  fctop  22891  cctop  22893  ntrfval  22911  elcls  22960  clsndisj  22962  elcls3  22970  neindisj2  23010  tgrest  23046  restco  23051  restsn  23057  restcld  23059  restcldi  23060  restopnb  23062  neitr  23067  restcls  23068  ordtbaslem  23075  ordtrest2lem  23090  hausnei2  23240  cnhaus  23241  regsep2  23263  dishaus  23269  ordthauslem  23270  cmpsublem  23286  cmpsub  23287  nconnsubb  23310  connsubclo  23311  1stcelcls  23348  islly  23355  cldllycmp  23382  lly1stc  23383  locfincmp  23413  elkgen  23423  ptclsg  23502  dfac14lem  23504  txrest  23518  pthaus  23525  txhaus  23534  xkohaus  23540  xkoptsub  23541  regr1lem  23626  isfbas  23716  fbasssin  23723  fbun  23727  isfil  23734  fbunfip  23756  fgval  23757  filconn  23770  uzrest  23784  isufil2  23795  hauspwpwf1  23874  fclsopni  23902  fclsnei  23906  fclsrest  23911  fcfnei  23922  fcfneii  23924  tsmsfbas  24015  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ust0  24107  trust  24117  restutopopn  24126  lpbl  24391  methaus  24408  metrest  24412  restmetu  24458  qtopbaslem  24646  qdensere  24657  xrtgioo  24695  metnrmlem3  24750  icoopnst  24836  iocopnst  24837  ovolicc2lem2  25419  ovolicc2lem5  25422  mblsplit  25433  limcnlp  25779  ellimc3  25780  limcflf  25782  limciun  25795  ig1pval  26081  shincl  31310  shmodi  31319  omlsi  31333  pjoml  31365  chm0  31420  chincl  31428  chdmm1  31454  ledi  31469  cmbr  31513  cmbr3  31537  mdbr  32223  dmdmd  32229  dmdi  32231  dmdbr3  32234  dmdbr4  32235  mdslmd1lem4  32257  cvmd  32265  cvexch  32303  dmdbr6ati  32352  mddmdin0i  32360  difeq  32447  ofpreima2  32590  ssdifidlprm  33429  ufdprmidl  33512  1arithufdlem4  33518  rspectopn  33857  ordtrest2NEWlem  33912  inelsros  34168  diffiunisros  34169  measvuni  34204  measinb  34211  inelcarsg  34302  carsgclctunlem2  34310  totprob  34418  ballotlemgval  34515  cvmscbv  35245  cvmsdisj  35257  cvmsss2  35261  satfv1  35350  nepss  35705  brapply  35926  opnbnd  36313  isfne  36327  tailfb  36365  bj-restsn  37070  bj-restpw  37080  bj-rest0  37081  bj-restb  37082  nlpfvineqsn  37397  fvineqsnf1  37398  pibt2  37405  ptrest  37613  poimirlem30  37644  mblfinlem2  37652  bndss  37780  qsdisjALTV  38606  redundss3  38619  lcvexchlem4  39030  fipjust  43554  ntrkbimka  44027  ntrk0kbimka  44028  clsk3nimkb  44029  isotone2  44038  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ismnushort  44290  relpfrlem  44943  permac8prim  45004  elrestd  45102  restsubel  45147  islptre  45617  islpcn  45637  subsaliuncllem  46355  subsaliuncl  46356  nnfoctbdjlem  46453  caragensplit  46498  vonvolmbllem  46658  vonvolmbl  46659  incsmflem  46739  decsmflem  46764  smflimlem2  46770  smflimlem3  46771  smflim  46775  smfpimcclem  46805  uzlidlring  48223  rngcvalALTV  48253  ringcvalALTV  48277  sepfsepc  48916  iscnrm3rlem2  48929  iscnrm3rlem8  48935  iscnrm3llem2  48938