Theorem ineq1 4136

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  {crab 3067   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  ineq2  4137  ineq12  4138  ineq1i  4139  ineq1d  4142  unineq  4208  dfrab3ss  4243  disjeq0  4386  intprgOLD  4912  inex1g  5238  reseq1  5874  sspred  6200  isofrlem  7191  qsdisj  8541  fiint  9021  elfiun  9119  dffi3  9120  inf3lema  9312  dfac5lem5  9814  kmlem12  9848  kmlem14  9850  fin23lem24  10009  fin23lem26  10012  fin23lem23  10013  fin23lem22  10014  fin23lem27  10015  ingru  10502  uzin2  14984  incexclem  15476  elrestr  17056  firest  17060  inopn  21956  isbasisg  22005  basis1  22008  basis2  22009  tgval  22013  fctop  22062  cctop  22064  ntrfval  22083  elcls  22132  clsndisj  22134  elcls3  22142  neindisj2  22182  tgrest  22218  restco  22223  restsn  22229  restcld  22231  restcldi  22232  restopnb  22234  neitr  22239  restcls  22240  ordtbaslem  22247  ordtrest2lem  22262  hausnei2  22412  cnhaus  22413  regsep2  22435  dishaus  22441  ordthauslem  22442  cmpsublem  22458  cmpsub  22459  nconnsubb  22482  connsubclo  22483  1stcelcls  22520  islly  22527  cldllycmp  22554  lly1stc  22555  locfincmp  22585  elkgen  22595  ptclsg  22674  dfac14lem  22676  txrest  22690  pthaus  22697  txhaus  22706  xkohaus  22712  xkoptsub  22713  regr1lem  22798  isfbas  22888  fbasssin  22895  fbun  22899  isfil  22906  fbunfip  22928  fgval  22929  filconn  22942  uzrest  22956  isufil2  22967  hauspwpwf1  23046  fclsopni  23074  fclsnei  23078  fclsrest  23083  fcfnei  23094  fcfneii  23096  tsmsfbas  23187  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ust0  23279  trust  23289  restutopopn  23298  lpbl  23565  methaus  23582  metrest  23586  restmetu  23632  qtopbaslem  23828  qdensere  23839  xrtgioo  23875  metnrmlem3  23930  icoopnst  24008  iocopnst  24009  ovolicc2lem2  24587  ovolicc2lem5  24590  mblsplit  24601  limcnlp  24947  ellimc3  24948  limcflf  24950  limciun  24963  ig1pval  25242  shincl  29644  shmodi  29653  omlsi  29667  pjoml  29699  chm0  29754  chincl  29762  chdmm1  29788  ledi  29803  cmbr  29847  cmbr3  29871  mdbr  30557  dmdmd  30563  dmdi  30565  dmdbr3  30568  dmdbr4  30569  mdslmd1lem4  30591  cvmd  30599  cvexch  30637  dmdbr6ati  30686  mddmdin0i  30694  difeq  30766  ofpreima2  30905  rspectopn  31719  ordtrest2NEWlem  31774  inelsros  32046  diffiunisros  32047  measvuni  32082  measinb  32089  inelcarsg  32178  carsgclctunlem2  32186  totprob  32294  ballotlemgval  32390  cvmscbv  33120  cvmsdisj  33132  cvmsss2  33136  satfv1  33225  nepss  33564  brapply  34167  opnbnd  34441  isfne  34455  tailfb  34493  bj-restsn  35180  bj-restpw  35190  bj-rest0  35191  bj-restb  35192  nlpfvineqsn  35507  fvineqsnf1  35508  pibt2  35515  ptrest  35703  poimirlem30  35734  mblfinlem2  35742  bndss  35871  qsdisjALTV  36655  redundss3  36668  lcvexchlem4  36978  fipjust  41061  ntrkbimka  41537  ntrk0kbimka  41538  clsk3nimkb  41539  isotone2  41548  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  ismnushort  41808  elrestd  42547  islptre  43050  islpcn  43070  subsaliuncllem  43786  subsaliuncl  43787  nnfoctbdjlem  43883  caragensplit  43928  vonvolmbllem  44088  vonvolmbl  44089  incsmflem  44164  decsmflem  44188  smflimlem2  44194  smflimlem3  44195  smflim  44199  smfpimcclem  44227  uzlidlring  45375  rngcvalALTV  45407  rngcval  45408  ringcvalALTV  45453  ringcval  45454  sepfsepc  46109  iscnrm3rlem2  46123  iscnrm3rlem8  46129  iscnrm3llem2  46132