Theorem ineq2i 3455

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

Hypothesis

Ref	Expression
ineq1i.1	|- A = B

Assertion

Ref	Expression
ineq2i	|- (C i^i A) = (C i^i B)

Proof of Theorem ineq2i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 |- A = B
2		ineq2 3452	. 2 |- (A = B -> (C i^i A) = (C i^i B))
3	1, 2	ax-mp 5	1 |- (C i^i A) = (C i^i B)

Syntax hints:   = wceq 1642   i^i cin 3209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214

This theorem is referenced by:  in4  3472  inindir  3474  indif2  3499  difun1  3515  dfrab3ss  3534  undif1  3626  difdifdir  3638  dfif3  3673  dfif5  3675  intunsn  3966  rint0  3967  riin0  4040  inindif  4076  ssfin  4471  spfinex  4538  res0  4978  resres  4981  resundi  4982  resindi  4984  inres  4986  resopab  5000  dminxp  5062  resdmres  5079  funimacnv  5169  sbthlem1  6204