Theorem ineq2 4235

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 4234	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
2		incom 4230	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4230	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   = wceq 1537   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  ineq12  4236  ineq2i  4238  ineq2d  4241  uneqin  4308  wefrc  5694  onfr  6434  onnseq  8400  qsdisj  8852  disjenex  9201  fiint  9394  fiintOLD  9395  elfiun  9499  dffi3  9500  cplem2  9959  dfac5  10198  kmlem2  10221  kmlem13  10232  kmlem14  10233  ackbij1lem16  10303  fin23lem12  10400  fin23lem19  10405  fin23lem33  10414  uzin2  15393  pgpfac1lem3  20121  pgpfac1lem5  20123  pgpfac1  20124  inopn  22926  basis1  22978  basis2  22979  baspartn  22982  fctop  23032  cctop  23034  ordtbaslem  23217  hausnei2  23382  cnhaus  23383  nrmsep  23386  isnrm2  23387  dishaus  23411  ordthauslem  23412  dfconn2  23448  nconnsubb  23452  finlocfin  23549  dissnlocfin  23558  locfindis  23559  kgeni  23566  pthaus  23667  txhaus  23676  xkohaus  23682  regr1lem  23768  fbasssin  23865  fbun  23869  fbunfip  23898  filconn  23912  isufil2  23937  ufileu  23948  filufint  23949  fmfnfmlem4  23986  fmfnfm  23987  fclsopni  24044  fclsbas  24050  fclsrest  24053  isfcf  24063  tsmsfbas  24157  ustincl  24237  ust0  24249  metreslem  24393  methaus  24554  qtopbaslem  24800  metnrmlem3  24902  ismbl  25580  shincl  31413  chincl  31531  chdmm1  31557  ledi  31572  cmbr  31616  cmbr3i  31632  cmbr3  31640  pjoml2  31643  stcltrlem1  32308  mdbr  32326  dmdbr  32331  cvmd  32368  cvexch  32406  sumdmdii  32447  mddmdin0i  32463  ofpreima2  32684  ssdifidllem  33449  ssdifidl  33450  ssdifidlprm  33451  1arithufdlem4  33540  crefeq  33791  ldgenpisyslem1  34127  ldgenpisys  34130  inelsros  34142  diffiunisros  34143  elcarsg  34270  carsgclctunlem2  34284  carsgclctun  34286  ballotlemfval  34454  ballotlemgval  34488  cvmscbv  35226  cvmsdisj  35238  cvmsss2  35242  satfv1  35331  nepss  35680  tailfb  36343  bj-0int  37067  mblfinlem2  37618  qsdisjALTV  38571  lshpinN  38945  elrfi  42650  fipjust  43527  conrel1d  43625  ntrk0kbimka  44001  clsk3nimkb  44002  isotone2  44011  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  csbresgVD  44866  disjf1  45090  qinioo  45453  fouriersw  46152  nnfoctbdjlem  46376  meadjun  46383  caragenel  46416  sepnsepolem2  48602  sepfsepc  48607  iscnrm3rlem8  48627  iscnrm3llem2  48630