Theorem ineq1 4172

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

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

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 3403  df-in 3918

This theorem is referenced by:  ineq2  4173  ineq12  4174  ineq1i  4175  ineq1d  4178  unineq  4247  dfrab3ss  4282  disjeq0  4415  inex1g  5269  reseq1  5933  sspred  6271  isofrlem  7297  qsdisj  8744  fiint  9253  fiintOLD  9254  elfiun  9357  dffi3  9358  inf3lema  9553  dfac5lem5  10056  kmlem12  10091  kmlem14  10093  fin23lem24  10251  fin23lem26  10254  fin23lem23  10255  fin23lem22  10256  fin23lem27  10257  ingru  10744  uzin2  15287  incexclem  15778  elrestr  17367  firest  17371  rngcval  20503  ringcval  20532  inopn  22762  isbasisg  22810  basis1  22813  basis2  22814  tgval  22818  fctop  22867  cctop  22869  ntrfval  22887  elcls  22936  clsndisj  22938  elcls3  22946  neindisj2  22986  tgrest  23022  restco  23027  restsn  23033  restcld  23035  restcldi  23036  restopnb  23038  neitr  23043  restcls  23044  ordtbaslem  23051  ordtrest2lem  23066  hausnei2  23216  cnhaus  23217  regsep2  23239  dishaus  23245  ordthauslem  23246  cmpsublem  23262  cmpsub  23263  nconnsubb  23286  connsubclo  23287  1stcelcls  23324  islly  23331  cldllycmp  23358  lly1stc  23359  locfincmp  23389  elkgen  23399  ptclsg  23478  dfac14lem  23480  txrest  23494  pthaus  23501  txhaus  23510  xkohaus  23516  xkoptsub  23517  regr1lem  23602  isfbas  23692  fbasssin  23699  fbun  23703  isfil  23710  fbunfip  23732  fgval  23733  filconn  23746  uzrest  23760  isufil2  23771  hauspwpwf1  23850  fclsopni  23878  fclsnei  23882  fclsrest  23887  fcfnei  23898  fcfneii  23900  tsmsfbas  23991  ustincl  24071  ustdiag  24072  ustinvel  24073  ustexhalf  24074  ust0  24083  trust  24093  restutopopn  24102  lpbl  24367  methaus  24384  metrest  24388  restmetu  24434  qtopbaslem  24622  qdensere  24633  xrtgioo  24671  metnrmlem3  24726  icoopnst  24812  iocopnst  24813  ovolicc2lem2  25395  ovolicc2lem5  25398  mblsplit  25409  limcnlp  25755  ellimc3  25756  limcflf  25758  limciun  25771  ig1pval  26057  shincl  31283  shmodi  31292  omlsi  31306  pjoml  31338  chm0  31393  chincl  31401  chdmm1  31427  ledi  31442  cmbr  31486  cmbr3  31510  mdbr  32196  dmdmd  32202  dmdi  32204  dmdbr3  32207  dmdbr4  32208  mdslmd1lem4  32230  cvmd  32238  cvexch  32276  dmdbr6ati  32325  mddmdin0i  32333  difeq  32420  ofpreima2  32563  ssdifidlprm  33402  ufdprmidl  33485  1arithufdlem4  33491  rspectopn  33830  ordtrest2NEWlem  33885  inelsros  34141  diffiunisros  34142  measvuni  34177  measinb  34184  inelcarsg  34275  carsgclctunlem2  34283  totprob  34391  ballotlemgval  34488  cvmscbv  35218  cvmsdisj  35230  cvmsss2  35234  satfv1  35323  nepss  35678  brapply  35899  opnbnd  36286  isfne  36300  tailfb  36338  bj-restsn  37043  bj-restpw  37053  bj-rest0  37054  bj-restb  37055  nlpfvineqsn  37370  fvineqsnf1  37371  pibt2  37378  ptrest  37586  poimirlem30  37617  mblfinlem2  37625  bndss  37753  qsdisjALTV  38579  redundss3  38592  lcvexchlem4  39003  fipjust  43527  ntrkbimka  44000  ntrk0kbimka  44001  clsk3nimkb  44002  isotone2  44011  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  ismnushort  44263  relpfrlem  44916  permac8prim  44977  elrestd  45075  restsubel  45120  islptre  45590  islpcn  45610  subsaliuncllem  46328  subsaliuncl  46329  nnfoctbdjlem  46426  caragensplit  46471  vonvolmbllem  46631  vonvolmbl  46632  incsmflem  46712  decsmflem  46737  smflimlem2  46743  smflimlem3  46744  smflim  46748  smfpimcclem  46778  uzlidlring  48196  rngcvalALTV  48226  ringcvalALTV  48250  sepfsepc  48889  iscnrm3rlem2  48902  iscnrm3rlem8  48908  iscnrm3llem2  48911