Theorem ineq1 4234

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  {crab 3443   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  ineq2  4235  ineq12  4236  ineq1i  4237  ineq1d  4240  unineq  4307  dfrab3ss  4342  disjeq0  4479  inex1g  5337  reseq1  6003  sspred  6341  isofrlem  7376  qsdisj  8852  fiint  9394  fiintOLD  9395  elfiun  9499  dffi3  9500  inf3lema  9693  dfac5lem5  10196  kmlem12  10231  kmlem14  10233  fin23lem24  10391  fin23lem26  10394  fin23lem23  10395  fin23lem22  10396  fin23lem27  10397  ingru  10884  uzin2  15393  incexclem  15884  elrestr  17488  firest  17492  rngcval  20640  ringcval  20669  inopn  22926  isbasisg  22975  basis1  22978  basis2  22979  tgval  22983  fctop  23032  cctop  23034  ntrfval  23053  elcls  23102  clsndisj  23104  elcls3  23112  neindisj2  23152  tgrest  23188  restco  23193  restsn  23199  restcld  23201  restcldi  23202  restopnb  23204  neitr  23209  restcls  23210  ordtbaslem  23217  ordtrest2lem  23232  hausnei2  23382  cnhaus  23383  regsep2  23405  dishaus  23411  ordthauslem  23412  cmpsublem  23428  cmpsub  23429  nconnsubb  23452  connsubclo  23453  1stcelcls  23490  islly  23497  cldllycmp  23524  lly1stc  23525  locfincmp  23555  elkgen  23565  ptclsg  23644  dfac14lem  23646  txrest  23660  pthaus  23667  txhaus  23676  xkohaus  23682  xkoptsub  23683  regr1lem  23768  isfbas  23858  fbasssin  23865  fbun  23869  isfil  23876  fbunfip  23898  fgval  23899  filconn  23912  uzrest  23926  isufil2  23937  hauspwpwf1  24016  fclsopni  24044  fclsnei  24048  fclsrest  24053  fcfnei  24064  fcfneii  24066  tsmsfbas  24157  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ust0  24249  trust  24259  restutopopn  24268  lpbl  24537  methaus  24554  metrest  24558  restmetu  24604  qtopbaslem  24800  qdensere  24811  xrtgioo  24847  metnrmlem3  24902  icoopnst  24988  iocopnst  24989  ovolicc2lem2  25572  ovolicc2lem5  25575  mblsplit  25586  limcnlp  25933  ellimc3  25934  limcflf  25936  limciun  25949  ig1pval  26235  shincl  31413  shmodi  31422  omlsi  31436  pjoml  31468  chm0  31523  chincl  31531  chdmm1  31557  ledi  31572  cmbr  31616  cmbr3  31640  mdbr  32326  dmdmd  32332  dmdi  32334  dmdbr3  32337  dmdbr4  32338  mdslmd1lem4  32360  cvmd  32368  cvexch  32406  dmdbr6ati  32455  mddmdin0i  32463  difeq  32548  ofpreima2  32684  ssdifidlprm  33451  ufdprmidl  33534  1arithufdlem4  33540  rspectopn  33813  ordtrest2NEWlem  33868  inelsros  34142  diffiunisros  34143  measvuni  34178  measinb  34185  inelcarsg  34276  carsgclctunlem2  34284  totprob  34392  ballotlemgval  34488  cvmscbv  35226  cvmsdisj  35238  cvmsss2  35242  satfv1  35331  nepss  35680  brapply  35902  opnbnd  36291  isfne  36305  tailfb  36343  bj-restsn  37048  bj-restpw  37058  bj-rest0  37059  bj-restb  37060  nlpfvineqsn  37375  fvineqsnf1  37376  pibt2  37383  ptrest  37579  poimirlem30  37610  mblfinlem2  37618  bndss  37746  qsdisjALTV  38571  redundss3  38584  lcvexchlem4  38993  fipjust  43527  ntrkbimka  44000  ntrk0kbimka  44001  clsk3nimkb  44002  isotone2  44011  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  ismnushort  44270  elrestd  45010  restsubel  45058  islptre  45540  islpcn  45560  subsaliuncllem  46278  subsaliuncl  46279  nnfoctbdjlem  46376  caragensplit  46421  vonvolmbllem  46581  vonvolmbl  46582  incsmflem  46662  decsmflem  46687  smflimlem2  46693  smflimlem3  46694  smflim  46698  smfpimcclem  46728  uzlidlring  47958  rngcvalALTV  47988  ringcvalALTV  48012  sepfsepc  48607  iscnrm3rlem2  48621  iscnrm3rlem8  48627  iscnrm3llem2  48630