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

Theorem ineq1 4006
Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)
Assertion
Ref Expression
ineq1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem ineq1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eleq2 2874 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 617 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elin 3995 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elin 3995 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 305 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2804 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2156  cin 3768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776
This theorem is referenced by:  ineq2  4007  ineq12  4008  ineq1i  4009  ineq1d  4012  unineq  4079  dfrab3ss  4106  disjeq0  4220  intprg  4703  inex1g  4996  reseq1  5591  sspred  5901  isofrlem  6810  qsdisj  8055  fiint  8472  elfiun  8571  dffi3  8572  inf3lema  8764  dfac5lem5  9229  kmlem12  9264  kmlem14  9266  fin23lem24  9425  fin23lem26  9428  fin23lem23  9429  fin23lem22  9430  fin23lem27  9431  ingru  9918  uzin2  14303  incexclem  14786  elrestr  16290  firest  16294  inopn  20913  isbasisg  20961  basis1  20964  basis2  20965  tgval  20969  fctop  21018  cctop  21020  ntrfval  21038  elcls  21087  clsndisj  21089  elcls3  21097  neindisj2  21137  tgrest  21173  restco  21178  restsn  21184  restcld  21186  restcldi  21187  restopnb  21189  neitr  21194  restcls  21195  ordtbaslem  21202  ordtrest2lem  21217  hausnei2  21367  cnhaus  21368  regsep2  21390  dishaus  21396  ordthauslem  21397  cmpsublem  21412  cmpsub  21413  nconnsubb  21436  connsubclo  21437  1stcelcls  21474  islly  21481  cldllycmp  21508  lly1stc  21509  locfincmp  21539  elkgen  21549  ptclsg  21628  dfac14lem  21630  txrest  21644  pthaus  21651  txhaus  21660  xkohaus  21666  xkoptsub  21667  regr1lem  21752  isfbas  21842  fbasssin  21849  fbun  21853  isfil  21860  fbunfip  21882  fgval  21883  filconn  21896  uzrest  21910  isufil2  21921  hauspwpwf1  22000  fclsopni  22028  fclsnei  22032  fclsrest  22037  fcfnei  22048  fcfneii  22050  tsmsfbas  22140  ustincl  22220  ustdiag  22221  ustinvel  22222  ustexhalf  22223  ust0  22232  trust  22242  restutopopn  22251  lpbl  22517  methaus  22534  metrest  22538  restmetu  22584  qtopbaslem  22771  qdensere  22782  xrtgioo  22818  metnrmlem3  22873  icoopnst  22947  iocopnst  22948  ovolicc2lem2  23495  ovolicc2lem5  23498  mblsplit  23509  limcnlp  23852  ellimc3  23853  limcflf  23855  limciun  23868  ig1pval  24142  shincl  28564  shmodi  28573  omlsi  28587  pjoml  28619  chm0  28674  chincl  28682  chdmm1  28708  ledi  28723  cmbr  28767  cmbr3  28791  mdbr  29477  dmdmd  29483  dmdi  29485  dmdbr3  29488  dmdbr4  29489  mdslmd1lem4  29511  cvmd  29519  cvexch  29557  dmdbr6ati  29606  mddmdin0i  29614  difeq  29676  ofpreima2  29789  ordtrest2NEWlem  30289  inelsros  30562  diffiunisros  30563  measvuni  30598  measinb  30605  inelcarsg  30694  carsgclctunlem2  30702  totprob  30810  ballotlemgval  30906  cvmscbv  31558  cvmsdisj  31570  cvmsss2  31574  nepss  31916  brapply  32361  opnbnd  32636  isfne  32650  tailfb  32688  bj-restsn  33341  bj-restpw  33351  bj-rest0  33352  bj-restb  33353  ptrest  33716  poimirlem30  33747  mblfinlem2  33755  bndss  33891  lcvexchlem4  34812  fipjust  38364  ntrkbimka  38830  ntrk0kbimka  38831  clsk3nimkb  38832  isotone2  38841  ntrclskb  38861  ntrclsk3  38862  ntrclsk13  38863  elrestd  39777  islptre  40325  islpcn  40345  subsaliuncllem  41048  subsaliuncl  41049  nnfoctbdjlem  41145  caragensplit  41190  vonvolmbllem  41350  vonvolmbl  41351  incsmflem  41426  decsmflem  41450  smflimlem2  41456  smflimlem3  41457  smflim  41461  smfpimcclem  41489  uzlidlring  42491  rngcvalALTV  42523  rngcval  42524  ringcvalALTV  42569  ringcval  42570
  Copyright terms: Public domain W3C validator