Theorem ineq12i 4118

Description: Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
ineq1i.1	⊢ 𝐴 = 𝐵
ineq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
ineq12i	⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

Proof of Theorem ineq12i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		ineq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		ineq12 4115	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094

This theorem is used by:  undir  4235  difundi  4238  difindir  4241  inrab  4264  inrab2  4265  elneldisj  4345  dfif4  4501  dfif5  4502  resindi  6002  resindir  6003  rninOLD  6156  inimass  6163  cnvrescnv  6206  cnvresid  6287  predin  6356  funtp  6627  orduniss2  7878  offres  8029  fodomr  9185  fodomfir  9357  epinid0  9636  cnvepnep  9646  wemapwe  9735  cotr3  15174  explecnv  16078  psssdm2  18805  ablfacrp  20333  cnfldfunALT  21745  pjfval2  22070  ofco2  22821  iundisj2  25925  clwwlknondisj  30759  lejdiri  32198  cmbr3i  32259  nonbooli  32310  5oai  32320  3oalem5  32325  mayetes3i  32388  mdexchi  32994  disjpreima  33276  disjxpin  33280  iundisj2f  33282  xppreima  33337  iundisj2fi  33485  xpinpreima  34649  xpinpreima2  34650  ordtcnvNEW  34663  pprodcnveq  36860  dfiota3  36900  bj-inrab  38055  ptrest  38805  ftc1anclem6  38884  dmxrn  39585  xrnres3  39625  br2coss  39726  1cosscnvxrn  39763  refsymrels2  39847  dfeqvrels2  39870  dfeldisj5  40011  dnwech  44321  fgraphopab  44466  onfrALTlem5  45785  onfrALTlem4  45786  onfrALTlem5VD  46127  onfrALTlem4VD  46128  disjxp1  46360  disjinfi  46480  oppczeroo  50690