Theorem ineq1 3807

Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)

Assertion

Ref	Expression
ineq1	⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Proof of Theorem ineq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2690	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 741	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3796	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3796	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 303	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	eqrdv 2620	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  ineq2  3808  ineq12  3809  ineq1i  3810  ineq1d  3813  unineq  3877  dfrab3ss  3905  intprg  4511  inex1g  4801  reseq1  5390  sspred  5688  isofrlem  6590  qsdisj  7824  fiint  8237  elfiun  8336  dffi3  8337  inf3lema  8521  dfac5lem5  8950  kmlem12  8983  kmlem14  8985  fin23lem24  9144  fin23lem26  9147  fin23lem23  9148  fin23lem22  9149  fin23lem27  9150  ingru  9637  uzin2  14084  incexclem  14568  elrestr  16089  firest  16093  inopn  20704  isbasisg  20751  basis1  20754  basis2  20755  tgval  20759  fctop  20808  cctop  20810  ntrfval  20828  elcls  20877  clsndisj  20879  elcls3  20887  neindisj2  20927  tgrest  20963  restco  20968  restsn  20974  restcld  20976  restcldi  20977  restopnb  20979  neitr  20984  restcls  20985  ordtbaslem  20992  ordtrest2lem  21007  hausnei2  21157  cnhaus  21158  regsep2  21180  dishaus  21186  ordthauslem  21187  cmpsublem  21202  cmpsub  21203  nconnsubb  21226  connsubclo  21227  1stcelcls  21264  islly  21271  cldllycmp  21298  lly1stc  21299  locfincmp  21329  elkgen  21339  ptclsg  21418  dfac14lem  21420  txrest  21434  pthaus  21441  txhaus  21450  xkohaus  21456  xkoptsub  21457  regr1lem  21542  isfbas  21633  fbasssin  21640  fbun  21644  isfil  21651  fbunfip  21673  fgval  21674  filconn  21687  uzrest  21701  isufil2  21712  hauspwpwf1  21791  fclsopni  21819  fclsnei  21823  fclsrest  21828  fcfnei  21839  fcfneii  21841  tsmsfbas  21931  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ust0  22023  trust  22033  restutopopn  22042  lpbl  22308  methaus  22325  metrest  22329  restmetu  22375  qtopbaslem  22562  qdensere  22573  xrtgioo  22609  metnrmlem3  22664  icoopnst  22738  iocopnst  22739  ovolicc2lem2  23286  ovolicc2lem5  23289  mblsplit  23300  limcnlp  23642  ellimc3  23643  limcflf  23645  limciun  23658  ig1pval  23932  shincl  28240  shmodi  28249  omlsi  28263  pjoml  28295  chm0  28350  chincl  28358  chdmm1  28384  ledi  28399  cmbr  28443  cmbr3  28467  mdbr  29153  dmdmd  29159  dmdi  29161  dmdbr3  29164  dmdbr4  29165  mdslmd1lem4  29187  cvmd  29195  cvexch  29233  dmdbr6ati  29282  mddmdin0i  29290  difeq  29355  ofpreima2  29466  ordtrest2NEWlem  29968  inelsros  30241  diffiunisros  30242  measvuni  30277  measinb  30284  inelcarsg  30373  carsgclctunlem2  30381  totprob  30489  ballotlemgval  30585  cvmscbv  31240  cvmsdisj  31252  cvmsss2  31256  nepss  31599  brapply  32045  opnbnd  32320  isfne  32334  tailfb  32372  bj-restsn  33035  bj-restpw  33045  bj-rest0  33046  bj-restb  33047  ptrest  33408  poimirlem30  33439  mblfinlem2  33447  bndss  33585  lcvexchlem4  34324  fipjust  37870  ntrkbimka  38336  ntrk0kbimka  38337  clsk3nimkb  38338  isotone2  38347  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  elrestd  39291  islptre  39851  islpcn  39871  subsaliuncllem  40575  subsaliuncl  40576  nnfoctbdjlem  40672  caragensplit  40714  vonvolmbllem  40874  vonvolmbl  40875  incsmflem  40950  decsmflem  40974  smflimlem2  40980  smflimlem3  40981  smflim  40985  smfpimcclem  41013  uzlidlring  41929  rngcvalALTV  41961  rngcval  41962  ringcvalALTV  42007  ringcval  42008