Theorem ineq1 4068

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

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  {crab 3092   ∩ cin 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-rab 3097  df-in 3836

This theorem is referenced by:  ineq2  4070  ineq12  4071  ineq1i  4072  ineq1d  4075  unineq  4141  dfrab3ss  4168  disjeq0  4288  intprg  4783  inex1g  5080  reseq1  5689  sspred  5994  isofrlem  6916  qsdisj  8174  fiint  8590  elfiun  8689  dffi3  8690  inf3lema  8881  dfac5lem5  9347  kmlem12  9381  kmlem14  9383  fin23lem24  9542  fin23lem26  9545  fin23lem23  9546  fin23lem22  9547  fin23lem27  9548  ingru  10035  uzin2  14565  incexclem  15051  elrestr  16558  firest  16562  inopn  21211  isbasisg  21259  basis1  21262  basis2  21263  tgval  21267  fctop  21316  cctop  21318  ntrfval  21336  elcls  21385  clsndisj  21387  elcls3  21395  neindisj2  21435  tgrest  21471  restco  21476  restsn  21482  restcld  21484  restcldi  21485  restopnb  21487  neitr  21492  restcls  21493  ordtbaslem  21500  ordtrest2lem  21515  hausnei2  21665  cnhaus  21666  regsep2  21688  dishaus  21694  ordthauslem  21695  cmpsublem  21711  cmpsub  21712  nconnsubb  21735  connsubclo  21736  1stcelcls  21773  islly  21780  cldllycmp  21807  lly1stc  21808  locfincmp  21838  elkgen  21848  ptclsg  21927  dfac14lem  21929  txrest  21943  pthaus  21950  txhaus  21959  xkohaus  21965  xkoptsub  21966  regr1lem  22051  isfbas  22141  fbasssin  22148  fbun  22152  isfil  22159  fbunfip  22181  fgval  22182  filconn  22195  uzrest  22209  isufil2  22220  hauspwpwf1  22299  fclsopni  22327  fclsnei  22331  fclsrest  22336  fcfnei  22347  fcfneii  22349  tsmsfbas  22439  ustincl  22519  ustdiag  22520  ustinvel  22521  ustexhalf  22522  ust0  22531  trust  22541  restutopopn  22550  lpbl  22816  methaus  22833  metrest  22837  restmetu  22883  qtopbaslem  23070  qdensere  23081  xrtgioo  23117  metnrmlem3  23172  icoopnst  23246  iocopnst  23247  ovolicc2lem2  23822  ovolicc2lem5  23825  mblsplit  23836  limcnlp  24179  ellimc3  24180  limcflf  24182  limciun  24195  ig1pval  24469  shincl  28939  shmodi  28948  omlsi  28962  pjoml  28994  chm0  29049  chincl  29057  chdmm1  29083  ledi  29098  cmbr  29142  cmbr3  29166  mdbr  29852  dmdmd  29858  dmdi  29860  dmdbr3  29863  dmdbr4  29864  mdslmd1lem4  29886  cvmd  29894  cvexch  29932  dmdbr6ati  29981  mddmdin0i  29989  difeq  30056  ofpreima2  30173  ordtrest2NEWlem  30815  inelsros  31088  diffiunisros  31089  measvuni  31124  measinb  31131  inelcarsg  31220  carsgclctunlem2  31228  totprob  31337  ballotlemgval  31433  cvmscbv  32096  cvmsdisj  32108  cvmsss2  32112  nepss  32474  brapply  32926  opnbnd  33200  isfne  33214  tailfb  33252  bj-restsn  33889  bj-restpw  33899  bj-rest0  33900  bj-restb  33901  nlpfvineqsn  34137  fvineqsnf1  34138  pibt2  34145  ptrest  34338  poimirlem30  34369  mblfinlem2  34377  bndss  34512  qsdisjALTV  35301  redundss3  35314  lcvexchlem4  35624  fipjust  39292  ntrkbimka  39757  ntrk0kbimka  39758  clsk3nimkb  39759  isotone2  39768  ntrclskb  39788  ntrclsk3  39789  ntrclsk13  39790  elrestd  40803  islptre  41337  islpcn  41357  subsaliuncllem  42077  subsaliuncl  42078  nnfoctbdjlem  42174  caragensplit  42219  vonvolmbllem  42379  vonvolmbl  42380  incsmflem  42455  decsmflem  42479  smflimlem2  42485  smflimlem3  42486  smflim  42490  smfpimcclem  42518  uzlidlring  43570  rngcvalALTV  43602  rngcval  43603  ringcvalALTV  43648  ringcval  43649