ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeltrd GIF version

Theorem eqeltrd 2192
Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
Hypotheses
Ref Expression
eqeltrd.1 (𝜑𝐴 = 𝐵)
eqeltrd.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqeltrd (𝜑𝐴𝐶)

Proof of Theorem eqeltrd
StepHypRef Expression
1 eqeltrd.2 . 2 (𝜑𝐵𝐶)
2 eqeltrd.1 . . 3 (𝜑𝐴 = 𝐵)
32eleq1d 2184 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 166 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  wcel 1463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  eqeltrrd  2193  3eltr4d  2199  eqeltrid  2202  syl6eqel  2206  ifcldadc  3469  ifcldcd  3475  intab  3768  disjiun  3892  iinexgm  4047  opexg  4118  tfisi  4469  nnpredcl  4504  imain  5173  fvmptd  5468  fvmptdf  5474  fvmptt  5478  elfvmptrab  5482  dffo3  5533  resfunexg  5607  f1oiso2  5694  riota2df  5716  riota5f  5720  ovmpodxf  5862  ovmpodf  5868  offval  5955  ofvalg  5957  offeq  5961  iunexg  5983  oprabexd  5991  fo1stresm  6025  fo2ndresm  6026  oprssdmm  6035  1stdm  6046  1stconst  6084  2ndconst  6085  cnvf1olem  6087  fo2ndf  6090  f1od2  6098  iunon  6147  tfrlemibacc  6189  tfrlemibfn  6191  tfr1onlembacc  6205  tfr1onlembfn  6207  tfrcllembacc  6218  tfrcllembfn  6220  tfrcl  6227  rdgon  6249  frec0g  6260  freccllem  6265  frecfcllem  6267  frecsuclem  6269  oacl  6322  omcl  6323  oeicl  6324  nntr2  6365  mptelixpg  6594  fidifsnen  6730  en2eqpr  6767  unfiin  6780  ssfirab  6788  fnfi  6791  relcnvfi  6795  fidcenumlemr  6809  elfi2  6826  supclti  6851  supubti  6852  suplubti  6853  supelti  6855  ordiso2  6886  djulclr  6900  djurclr  6901  djulcl  6902  djurcl  6903  djuss  6921  updjudhcoinlf  6931  updjudhcoinrg  6932  ctssdclemn0  6961  ctssdccl  6962  ctssdc  6964  enumctlemm  6965  cardcl  7003  addclpi  7099  mulclpi  7100  addclnq  7147  mulclnq  7148  addclnq0  7223  mulclnq0  7224  nqpnq0nq  7225  elnp1st2nd  7248  prarloclemcalc  7274  distrlem1prl  7354  distrlem1pru  7355  ltexprlemopl  7373  ltexprlemopu  7375  ltexprlemfl  7381  ltexprlemrl  7382  ltexprlemfu  7383  ltexprlemru  7384  addcanprlemu  7387  recexprlemloc  7403  aptiprleml  7411  caucvgprprlemopl  7469  suplocexprlemex  7494  addclsr  7525  mulclsr  7526  recexgt0sr  7545  mulextsr1lem  7552  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  axaddcl  7636  axaddrcl  7637  axmulcl  7638  axmulrcl  7639  axcaucvglemval  7669  subcl  7925  cru  8327  aprcl  8371  divclap  8401  redivclap  8454  diveqap1bd  8558  lbinfcl  8667  cju  8679  nn1m1nn  8698  nnsub  8719  nnnn0addcl  8961  un0addcl  8964  peano2z  9044  peano2zm  9046  zaddcllemneg  9047  zaddcl  9048  nnaddm1cl  9069  nn0n0n1ge2  9075  zdivadd  9094  zdivmul  9095  suprzclex  9103  zneo  9106  peano5uzti  9113  supinfneg  9342  infsupneg  9343  qmulz  9367  qnegcl  9380  qapne  9383  qdivcl  9387  cnref1o  9392  xnegcl  9566  xltnegi  9569  xaddnemnf  9591  xaddnepnf  9592  xnegdi  9602  xnpcan  9606  xltadd1  9610  xposdif  9616  xleaddadd  9621  iccf1o  9738  ige3m2fz  9780  ige2m1fz1  9840  rebtwn2z  9983  flqcl  9997  flapcl  9999  ceilqcl  10032  intfracq  10044  modqcl  10050  mulqmod0  10054  modqdifz  10060  zmodcl  10068  modfzo0difsn  10119  modsumfzodifsn  10120  frec2uzzd  10124  frec2uzsucd  10125  frec2uzuzd  10126  frecuzrdgrrn  10132  frec2uzrdg  10133  frecuzrdgrcl  10134  frecuzrdgsuc  10138  frecuzrdgrclt  10139  frecuzrdgg  10140  frecuzrdgsuctlem  10147  fzofig  10156  iseqovex  10180  seq3val  10182  seqvalcd  10183  seqf  10185  seqovcd  10187  seq3clss  10191  seq3caopr3  10205  iseqf1olemnab  10212  iseqf1olemqk  10218  iseqf1olemjpcl  10219  iseqf1olemqpcl  10220  iseqf1olemfvp  10221  seq3f1olemqsumkj  10222  seq3f1olemqsum  10224  seq3f1oleml  10227  seq3f1o  10228  seq3distr  10237  ser0f  10239  ser3le  10242  exp3vallem  10245  exp3val  10246  exp1  10250  expcl2lemap  10256  m1expcl2  10266  expaddzap  10288  sqcl  10305  nnsqcl  10313  qsqcl  10315  zesq  10361  facp1  10427  faccl  10432  facdiv  10435  bcval  10446  bcrpcl  10450  bcp1n  10458  bcpasc  10463  permnn  10468  hashennn  10477  hashcl  10478  shftlem  10539  ovshftex  10542  shftf  10553  seq3shft  10561  cjth  10569  imval  10573  recl  10576  imcl  10577  crre  10580  remim  10583  reim0b  10585  cvg1nlemcau  10707  uzin2  10710  resqrexlem1arp  10728  resqrexlemp1rp  10729  resqrexlemglsq  10745  resqrexlemga  10746  resqrtcl  10752  abscl  10774  absrpclap  10784  nn0abscl  10808  fzomaxdiflem  10835  fzomaxdif  10836  maxabslemab  10929  maxcl  10933  zmaxcl  10947  minmax  10952  mincl  10953  xrmaxcl  10972  xrmaxaddlem  10980  xrminmax  10985  xrmincl  10986  xrmineqinf  10989  xrminrpcl  10994  reccn2ap  11033  climaddc1  11049  climmulc2  11051  climsubc1  11052  climsubc2  11053  climle  11054  climlec2  11061  climcvg1nlem  11069  sumrbdclem  11096  fsum3cvg  11097  summodclem3  11100  summodclem2a  11101  zsumdc  11104  fsumgcl  11106  fsum3  11107  isumss  11111  fisumss  11112  isumss2  11113  fsum3cvg2  11114  fsum3ser  11117  fsumcl2lem  11118  fsumcllem  11119  fsumadd  11126  sumsnf  11129  fsumsplitsn  11130  isumcl  11145  isummulc2  11146  isumrecl  11149  isumge0  11150  isumadd  11151  fsum2dlemstep  11154  fisumcom2  11158  mptfzshft  11162  fsumrev  11163  fsummulc2  11168  iserabs  11195  isumshft  11210  isumsplit  11211  isum1p  11212  isumrpcl  11214  isumle  11215  isumlessdc  11216  trireciplem  11220  expcnvap0  11222  expcnvre  11223  expcnv  11224  explecnv  11225  geolim  11231  geolim2  11232  geo2lim  11236  cvgratnnlemsumlt  11248  cvgratz  11252  mertenslemub  11254  mertenslemi1  11255  mertenslem2  11256  mertensabs  11257  efcllemp  11274  ef0lem  11276  efcvgfsum  11283  reefcl  11284  ege2le3  11287  efcj  11289  efaddlem  11290  eftlcvg  11303  eftlcl  11304  reeftlcl  11305  eftlub  11306  efsep  11307  effsumlt  11308  efgt1p2  11311  efgt1p  11312  reeff1  11317  tanclap  11326  resincl  11337  recoscl  11338  retanclap  11339  eirraplem  11390  dvdsval2  11403  sqoddm1div8z  11490  zssinfcl  11548  infssuzex  11549  infssuzcldc  11551  gcdval  11555  gcdn0cl  11558  gcddvds  11559  divgcdnnr  11571  nn0seqcvgd  11629  ialgrlem1st  11630  ialgrlemconst  11631  algrf  11633  algrp1  11634  eucalgf  11643  eucalglt  11645  lcmval  11651  lcmcllem  11655  lcmgcdlem  11665  cncongr2  11692  sqrt2irrlem  11746  oddpwdclemxy  11753  oddpwdclemdc  11757  qden1elz  11789  phicl2  11796  phimullem  11807  ennnfonelemjn  11821  ennnfonelemg  11822  ennnfonelemp1  11825  ctinfomlemom  11846  ctiunctlemfo  11858  setsex  11897  strsetsid  11898  ressid2  11924  ressval2  11925  ressid  11926  iunopn  12075  toponmax  12098  tgvalex  12125  tgtop  12143  tgiun  12148  tgidm  12149  ntropn  12192  tgrest  12244  restopnb  12256  cnovex  12271  cnclima  12298  txvalex  12329  txtop  12335  tx1cn  12344  tx2cn  12345  txcnp  12346  txcnmpt  12348  txdis1cn  12353  cnmptcom  12373  imasnopn  12374  hmeocnv  12382  hmeores  12390  txhmeo  12394  txswaphmeo  12396  ispsmet  12398  xmetres  12457  metres  12458  blex  12462  xmeter  12511  xmetresbl  12515  mopntopon  12518  isxms2  12527  xmetxp  12582  xmettx  12585  txmetcnp  12593  qtopbasss  12596  qtopbas  12597  reopnap  12613  ioo2blex  12619  blssioo  12620  tgioo  12621  fsumcncntop  12631  cncfval  12634  divccncfap  12652  cdivcncfap  12662  ivthdec  12697  limccnpcntop  12719  dvrecap  12752  djucllem  12841  nninfsellemeq  13044  qdencn  13056  isomninnlem  13059  cvgcmp2nlemabs  13061  trilpolemclim  13063  trilpolemisumle  13065  trilpolemeq1  13067  trilpolemlt1  13068
  Copyright terms: Public domain W3C validator