Theorem ineq1 4181

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  {crab 3142   ∩ cin 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3943

This theorem is referenced by:  ineq2  4183  ineq12  4184  ineq1i  4185  ineq1d  4188  unineq  4254  dfrab3ss  4281  disjeq0  4405  intprg  4910  inex1g  5223  reseq1  5847  sspred  6156  isofrlem  7093  qsdisj  8374  fiint  8795  elfiun  8894  dffi3  8895  inf3lema  9087  dfac5lem5  9553  kmlem12  9587  kmlem14  9589  fin23lem24  9744  fin23lem26  9747  fin23lem23  9748  fin23lem22  9749  fin23lem27  9750  ingru  10237  uzin2  14704  incexclem  15191  elrestr  16702  firest  16706  inopn  21507  isbasisg  21555  basis1  21558  basis2  21559  tgval  21563  fctop  21612  cctop  21614  ntrfval  21632  elcls  21681  clsndisj  21683  elcls3  21691  neindisj2  21731  tgrest  21767  restco  21772  restsn  21778  restcld  21780  restcldi  21781  restopnb  21783  neitr  21788  restcls  21789  ordtbaslem  21796  ordtrest2lem  21811  hausnei2  21961  cnhaus  21962  regsep2  21984  dishaus  21990  ordthauslem  21991  cmpsublem  22007  cmpsub  22008  nconnsubb  22031  connsubclo  22032  1stcelcls  22069  islly  22076  cldllycmp  22103  lly1stc  22104  locfincmp  22134  elkgen  22144  ptclsg  22223  dfac14lem  22225  txrest  22239  pthaus  22246  txhaus  22255  xkohaus  22261  xkoptsub  22262  regr1lem  22347  isfbas  22437  fbasssin  22444  fbun  22448  isfil  22455  fbunfip  22477  fgval  22478  filconn  22491  uzrest  22505  isufil2  22516  hauspwpwf1  22595  fclsopni  22623  fclsnei  22627  fclsrest  22632  fcfnei  22643  fcfneii  22645  tsmsfbas  22736  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ust0  22828  trust  22838  restutopopn  22847  lpbl  23113  methaus  23130  metrest  23134  restmetu  23180  qtopbaslem  23367  qdensere  23378  xrtgioo  23414  metnrmlem3  23469  icoopnst  23543  iocopnst  23544  ovolicc2lem2  24119  ovolicc2lem5  24122  mblsplit  24133  limcnlp  24476  ellimc3  24477  limcflf  24479  limciun  24492  ig1pval  24766  shincl  29158  shmodi  29167  omlsi  29181  pjoml  29213  chm0  29268  chincl  29276  chdmm1  29302  ledi  29317  cmbr  29361  cmbr3  29385  mdbr  30071  dmdmd  30077  dmdi  30079  dmdbr3  30082  dmdbr4  30083  mdslmd1lem4  30105  cvmd  30113  cvexch  30151  dmdbr6ati  30200  mddmdin0i  30208  difeq  30280  ofpreima2  30411  ordtrest2NEWlem  31165  inelsros  31437  diffiunisros  31438  measvuni  31473  measinb  31480  inelcarsg  31569  carsgclctunlem2  31577  totprob  31685  ballotlemgval  31781  cvmscbv  32505  cvmsdisj  32517  cvmsss2  32521  satfv1  32610  nepss  32948  brapply  33399  opnbnd  33673  isfne  33687  tailfb  33725  bj-restsn  34376  bj-restpw  34386  bj-rest0  34387  bj-restb  34388  nlpfvineqsn  34693  fvineqsnf1  34694  pibt2  34701  ptrest  34906  poimirlem30  34937  mblfinlem2  34945  bndss  35079  qsdisjALTV  35865  redundss3  35878  lcvexchlem4  36188  fipjust  39944  ntrkbimka  40408  ntrk0kbimka  40409  clsk3nimkb  40410  isotone2  40419  ntrclskb  40439  ntrclsk3  40440  ntrclsk13  40441  elrestd  41394  islptre  41920  islpcn  41940  subsaliuncllem  42660  subsaliuncl  42661  nnfoctbdjlem  42757  caragensplit  42802  vonvolmbllem  42962  vonvolmbl  42963  incsmflem  43038  decsmflem  43062  smflimlem2  43068  smflimlem3  43069  smflim  43073  smfpimcclem  43101  uzlidlring  44220  rngcvalALTV  44252  rngcval  44253  ringcvalALTV  44298  ringcval  44299