Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineq12i Structured version   Visualization version   GIF version

Theorem ineq12i 4137
 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
StepHypRef Expression
1 ineq1i.1 . 2 𝐴 = 𝐵
2 ineq12i.2 . 2 𝐶 = 𝐷
3 ineq12 4134 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3mp2an 691 1 (𝐴𝐶) = (𝐵𝐷)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∩ cin 3880 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888 This theorem is referenced by:  undir  4203  difundi  4206  difindir  4209  inrab  4227  inrab2  4228  elneldisj  4296  dfif4  4440  dfif5  4441  inxp  5667  resindi  5834  resindir  5835  rnin  5972  inimass  5979  cnvrescnv  6019  predin  6139  funtp  6381  orduniss2  7530  offres  7668  fodomr  8654  epinid0  9050  cnvepnep  9057  wemapwe  9146  cotr3  14331  explecnv  15214  psssdm2  17819  ablfacrp  19184  cnfldfun  20106  pjfval2  20402  ofco2  21063  iundisj2  24160  clwwlknondisj  27903  lejdiri  29329  cmbr3i  29390  nonbooli  29441  5oai  29451  3oalem5  29456  mayetes3i  29519  mdexchi  30125  disjpreima  30354  disjxpin  30358  iundisj2f  30360  xppreima  30415  iundisj2fi  30553  xpinpreima  31271  xpinpreima2  31272  ordtcnvNEW  31285  pprodcnveq  33469  dfiota3  33509  bj-inrab  34385  ptrest  35072  ftc1anclem6  35151  xrnres3  35828  br2coss  35859  1cosscnvxrn  35891  refsymrels2  35977  dfeqvrels2  35999  dfeldisj5  36130  dnwech  40007  fgraphopab  40169  onfrALTlem5  41263  onfrALTlem4  41264  onfrALTlem5VD  41606  onfrALTlem4VD  41607  disjxp1  41718  disjinfi  41835
 Copyright terms: Public domain W3C validator