Theorem ineq2 4207

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

Assertion

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

Proof of Theorem ineq2

Step	Hyp	Ref	Expression
1		ineq1 4206	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
2		incom 4202	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4202	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3956

This theorem is referenced by:  ineq12  4208  ineq2i  4210  ineq2d  4213  uneqin  4279  intprgOLD  4989  wefrc  5671  onfr  6404  onnseq  8344  qsdisj  8788  disjenex  9135  fiint  9324  elfiun  9425  dffi3  9426  cplem2  9885  dfac5  10123  kmlem2  10146  kmlem13  10157  kmlem14  10158  ackbij1lem16  10230  fin23lem12  10326  fin23lem19  10331  fin23lem33  10340  uzin2  15291  pgpfac1lem3  19947  pgpfac1lem5  19949  pgpfac1  19950  inopn  22401  basis1  22453  basis2  22454  baspartn  22457  fctop  22507  cctop  22509  ordtbaslem  22692  hausnei2  22857  cnhaus  22858  nrmsep  22861  isnrm2  22862  dishaus  22886  ordthauslem  22887  dfconn2  22923  nconnsubb  22927  finlocfin  23024  dissnlocfin  23033  locfindis  23034  kgeni  23041  pthaus  23142  txhaus  23151  xkohaus  23157  regr1lem  23243  fbasssin  23340  fbun  23344  fbunfip  23373  filconn  23387  isufil2  23412  ufileu  23423  filufint  23424  fmfnfmlem4  23461  fmfnfm  23462  fclsopni  23519  fclsbas  23525  fclsrest  23528  isfcf  23538  tsmsfbas  23632  ustincl  23712  ust0  23724  metreslem  23868  methaus  24029  qtopbaslem  24275  metnrmlem3  24377  ismbl  25043  shincl  30634  chincl  30752  chdmm1  30778  ledi  30793  cmbr  30837  cmbr3i  30853  cmbr3  30861  pjoml2  30864  stcltrlem1  31529  mdbr  31547  dmdbr  31552  cvmd  31589  cvexch  31627  sumdmdii  31668  mddmdin0i  31684  ofpreima2  31891  crefeq  32825  ldgenpisyslem1  33161  ldgenpisys  33164  inelsros  33176  diffiunisros  33177  elcarsg  33304  carsgclctunlem2  33318  carsgclctun  33320  ballotlemfval  33488  ballotlemgval  33522  cvmscbv  34249  cvmsdisj  34261  cvmsss2  34265  satfv1  34354  nepss  34687  tailfb  35262  bj-0int  35982  mblfinlem2  36526  qsdisjALTV  37485  lshpinN  37859  elrfi  41432  fipjust  42316  conrel1d  42414  ntrk0kbimka  42790  clsk3nimkb  42791  isotone2  42800  ntrclskb  42820  ntrclsk3  42821  ntrclsk13  42822  csbresgVD  43656  disjf1  43880  qinioo  44248  fouriersw  44947  nnfoctbdjlem  45171  meadjun  45178  caragenel  45211  sepnsepolem2  47555  sepfsepc  47560  iscnrm3rlem8  47580  iscnrm3llem2  47583