Theorem ineq1 4193

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938

This theorem is referenced by:  ineq2  4194  ineq12  4195  ineq1i  4196  ineq1d  4199  unineq  4268  dfrab3ss  4303  disjeq0  4436  inex1g  5294  reseq1  5965  sspred  6304  isofrlem  7338  qsdisj  8813  fiint  9343  fiintOLD  9344  elfiun  9447  dffi3  9448  inf3lema  9643  dfac5lem5  10146  kmlem12  10181  kmlem14  10183  fin23lem24  10341  fin23lem26  10344  fin23lem23  10345  fin23lem22  10346  fin23lem27  10347  ingru  10834  uzin2  15368  incexclem  15857  elrestr  17447  firest  17451  rngcval  20583  ringcval  20612  inopn  22842  isbasisg  22890  basis1  22893  basis2  22894  tgval  22898  fctop  22947  cctop  22949  ntrfval  22967  elcls  23016  clsndisj  23018  elcls3  23026  neindisj2  23066  tgrest  23102  restco  23107  restsn  23113  restcld  23115  restcldi  23116  restopnb  23118  neitr  23123  restcls  23124  ordtbaslem  23131  ordtrest2lem  23146  hausnei2  23296  cnhaus  23297  regsep2  23319  dishaus  23325  ordthauslem  23326  cmpsublem  23342  cmpsub  23343  nconnsubb  23366  connsubclo  23367  1stcelcls  23404  islly  23411  cldllycmp  23438  lly1stc  23439  locfincmp  23469  elkgen  23479  ptclsg  23558  dfac14lem  23560  txrest  23574  pthaus  23581  txhaus  23590  xkohaus  23596  xkoptsub  23597  regr1lem  23682  isfbas  23772  fbasssin  23779  fbun  23783  isfil  23790  fbunfip  23812  fgval  23813  filconn  23826  uzrest  23840  isufil2  23851  hauspwpwf1  23930  fclsopni  23958  fclsnei  23962  fclsrest  23967  fcfnei  23978  fcfneii  23980  tsmsfbas  24071  ustincl  24151  ustdiag  24152  ustinvel  24153  ustexhalf  24154  ust0  24163  trust  24173  restutopopn  24182  lpbl  24447  methaus  24464  metrest  24468  restmetu  24514  qtopbaslem  24702  qdensere  24713  xrtgioo  24751  metnrmlem3  24806  icoopnst  24892  iocopnst  24893  ovolicc2lem2  25476  ovolicc2lem5  25479  mblsplit  25490  limcnlp  25836  ellimc3  25837  limcflf  25839  limciun  25852  ig1pval  26138  shincl  31367  shmodi  31376  omlsi  31390  pjoml  31422  chm0  31477  chincl  31485  chdmm1  31511  ledi  31526  cmbr  31570  cmbr3  31594  mdbr  32280  dmdmd  32286  dmdi  32288  dmdbr3  32291  dmdbr4  32292  mdslmd1lem4  32314  cvmd  32322  cvexch  32360  dmdbr6ati  32409  mddmdin0i  32417  difeq  32504  ofpreima2  32649  ssdifidlprm  33478  ufdprmidl  33561  1arithufdlem4  33567  rspectopn  33903  ordtrest2NEWlem  33958  inelsros  34214  diffiunisros  34215  measvuni  34250  measinb  34257  inelcarsg  34348  carsgclctunlem2  34356  totprob  34464  ballotlemgval  34561  cvmscbv  35285  cvmsdisj  35297  cvmsss2  35301  satfv1  35390  nepss  35740  brapply  35961  opnbnd  36348  isfne  36362  tailfb  36400  bj-restsn  37105  bj-restpw  37115  bj-rest0  37116  bj-restb  37117  nlpfvineqsn  37432  fvineqsnf1  37433  pibt2  37440  ptrest  37648  poimirlem30  37679  mblfinlem2  37687  bndss  37815  qsdisjALTV  38638  redundss3  38651  lcvexchlem4  39060  fipjust  43564  ntrkbimka  44037  ntrk0kbimka  44038  clsk3nimkb  44039  isotone2  44048  ntrclskb  44068  ntrclsk3  44069  ntrclsk13  44070  ismnushort  44300  relpfrlem  44953  permac8prim  45014  elrestd  45112  restsubel  45157  islptre  45628  islpcn  45648  subsaliuncllem  46366  subsaliuncl  46367  nnfoctbdjlem  46464  caragensplit  46509  vonvolmbllem  46669  vonvolmbl  46670  incsmflem  46750  decsmflem  46775  smflimlem2  46781  smflimlem3  46782  smflim  46786  smfpimcclem  46816  uzlidlring  48190  rngcvalALTV  48220  ringcvalALTV  48244  sepfsepc  48882  iscnrm3rlem2  48895  iscnrm3rlem8  48901  iscnrm3llem2  48904