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

Theorem eleq1w 2866
Description: Weaker version of eleq1 2871 (but more general than elequ1 2163) not depending on ax-ext 2782 nor df-cleq 2797. (Contributed by BJ, 24-Jun-2019.)
Assertion
Ref Expression
eleq1w (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))

Proof of Theorem eleq1w
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 equequ2 2122 . . . 4 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
21anbi1d 617 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝑥𝑧𝐴) ↔ (𝑧 = 𝑦𝑧𝐴)))
32exbidv 2012 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥𝑧𝐴) ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴)))
4 df-clel 2800 . 2 (𝑥𝐴 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝐴))
5 df-clel 2800 . 2 (𝑦𝐴 ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴))
63, 4, 53bitr4g 305 1 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wex 1859  wcel 2156
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
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-clel 2800
This theorem is referenced by:  cleqh  2906  clelsb3  2911  nfcjust  2934  clelsb3f  2950  ralcom2  3290  nfrab  3310  cbvralf  3352  cbvreu  3356  cbvrab  3386  ralab2  3565  rexab2  3567  reu2  3590  reu6  3591  rmo4  3595  reu8  3598  2reu5  3612  ru  3630  difjust  3769  unjust  3771  injust  3773  dfss2f  3787  dfdif3  3917  eqeuel  4140  rabsnifsb  4446  eluniab  4639  elintab  4678  uniintsn  4704  dfiunv2  4746  disjxun  4840  cbvmptf  4940  cbvmpt  4941  isso2i  5262  dfres2  5656  imai  5686  wfisg  5926  tz7.7  5960  fvn0ssdmfun  6570  fmptco  6617  cbvriota  6843  cbvmpt2x  6961  tfis  7282  tfindes  7290  findes  7324  resiexg  7330  dfoprab4f  7456  fmpt2x  7467  wfrlem10  7658  smogt  7698  resixpfo  8181  ixpsnf1o  8183  dom2lem  8230  mapsnend  8269  pw2f1olem  8301  findcard3  8440  ordiso2  8657  elirrv  8738  cantnflem1d  8830  cantnf  8835  setind  8855  tz9.12lem3  8897  infxpen  9118  aceq1  9221  aceq2  9223  dfac12lem2  9249  kmlem4  9258  kmlem14  9268  cfsmolem  9375  sornom  9382  isf32lem9  9466  axdc2  9554  fpwwe2lem8  9742  fpwwe2  9748  wunex2  9843  dedekindle  10484  wloglei  10843  uzind4s  11964  seqof2  13080  reuccats1  13702  shftfn  14034  rexuz3  14309  zsum  14670  fsum  14672  sumss  14676  sumss2  14678  fsumcvg2  14679  fsumser  14682  fsumsplitf  14693  isumless  14797  prodfdiv  14847  cbvprod  14864  zprod  14886  fprod  14890  fprodntriv  14891  prodss  14896  fprod2dlem  14929  fproddivf  14936  fprodsplitf  14937  rpnnen2lem10  15170  cpnnen  15176  sumeven  15328  sumodd  15329  sadcp1  15394  smupp1  15419  pcmptdvds  15813  prmreclem2  15836  prmreclem5  15839  prmreclem6  15840  prmrec  15841  prmdvdsprmo  15961  iscatd2  16544  initoeu2  16868  yoniso  17128  mrcmndind  17569  symggen  18089  dprd2d2  18643  isdrngrd  18975  lbspss  19287  opsrtoslem1  19690  frlmphl  20328  frlmup1  20345  mdetralt  20623  mdetralt2  20624  mdetunilem2  20628  maducoeval2  20655  chfacfscmulgsum  20876  chfacfpmmulgsum  20880  isclo2  21104  neiptopnei  21148  ptcldmpt  21629  elmptrab  21842  hausflimi  21995  hausflim  21996  alexsubALTlem3  22064  alexsubALTlem4  22065  ptcmplem2  22068  cnextcn  22082  cnextfres1  22083  tgphaus  22131  ustuqtop  22261  utopsnneip  22263  ucncn  22300  nrmmetd  22590  xrhmeo  22956  iscau2  23285  caucfil  23291  cmetcaulem  23296  bcth  23336  vitalilem3  23589  vitali  23592  i1f1lem  23668  itg11  23670  i1fres  23684  mbfi1fseq  23700  mbfi1flim  23702  itg2uba  23722  itg2splitlem  23727  isibl2  23745  cbvitg  23754  itgss3  23793  dvmptfsum  23950  rolle  23965  elply2  24164  plyexmo  24280  lgamgulmlem2  24968  prmorcht  25116  pclogsum  25152  dchr1  25194  lgsdir  25269  lgsdilem2  25270  lgsdi  25271  lgsne0  25272  lgsquadlem3  25319  lgsquad  25320  2sqlem8  25363  legval  25691  legov  25692  tglineintmo  25749  tglowdim2ln  25758  ishpg  25863  lnopp2hpgb  25867  hpgerlem  25869  colopp  25873  axcontlem1  26056  numedglnl  26252  uvtxnbgrvtx  26511  cusgrres  26570  wspniunwspnon  27061  rusgrnumwwlkb0  27111  frgr3vlem2  27447  3vfriswmgrlem  27450  fusgr2wsp2nb  27507  numclwlk2lem2f1o  27557  numclwlk2lem2f1oOLD  27564  lpni  27661  pjhthmo  28487  chscllem2  28823  moel  29649  cbvdisjf  29708  fmptcof2  29782  aciunf1lem  29787  funcnv4mpt  29795  fpwrelmapffslem  29832  fsumiunle  29900  esumcvg  30471  fiunelros  30560  measiun  30604  bnj1146  31183  bnj1185  31185  bnj1385  31224  bnj1014  31351  bnj1112  31372  bnj1123  31375  bnj1228  31400  bnj1326  31415  bnj1321  31416  bnj1384  31421  bnj1417  31430  bnj1497  31449  mrsubrn  31731  dfon2lem6  32011  frpoinsg  32060  frinsg  32064  poseq  32072  soseq  32073  nosupno  32168  nosupdm  32169  nosupbnd1lem1  32173  noeta  32187  nocvxminlem  32212  dfbigcup2  32325  lineintmo  32583  bj-nfcjust  33158  mptsnunlem  33500  ptrest  33719  poimirlem25  33745  mblfinlem2  33758  mblfinlem3  33759  mblfinlem4  33760  ismblfin  33761  mbfposadd  33767  itg2addnclem  33771  ftc1anclem5  33799  ftc1anclem6  33800  ftc1anclem7  33801  ftc1anc  33803  areacirclem5  33814  fdc1  33851  inxprnres  34375  prtlem13  34645  prtlem16  34646  fsumshftd  34729  pmapglb  35548  polval2N  35684  osumcllem4N  35737  pexmidlem1N  35748  dih1dimatlem  37108  mapdh9a  37568  mapdh9aOLDN  37569  fphpd  37880  fphpdo  37881  pellex  37899  setindtrs  38091  dford3lem2  38093  fnwe2lem2  38120  mendlmod  38262  rababg  38377  fsovrfovd  38801  fsovcnvlem  38805  elunif  39667  iunincfi  39763  cbvmpt22  39768  cbvmpt21  39769  disjf1  39856  wessf1ornlem  39858  disjinfi  39867  supxrleubrnmptf  40157  monoordxr  40190  monoord2xr  40192  fsumclf  40279  fsummulc1f  40280  fsumnncl  40281  fsumf1of  40284  fsumiunss  40285  fsumreclf  40286  fsumlessf  40287  fsumsermpt  40289  fmulcl  40291  fmul01lt1lem2  40295  fprodexp  40304  fprodabs2  40305  climmulf  40314  climexp  40315  climrecf  40319  climinff  40321  climaddf  40325  mullimc  40326  limcperiod  40338  sumnnodd  40340  neglimc  40357  addlimc  40358  climsubmpt  40370  climreclf  40374  climeldmeqmpt  40378  climfveqmpt  40381  fnlimfvre  40384  climfveqf  40390  climfveqmpt3  40392  climeldmeqf  40393  climeqf  40398  climeldmeqmpt3  40399  climinf2  40417  limsupequz  40433  limsupequzmptf  40441  lmbr3  40457  cnrefiisp  40534  cncfshift  40565  fprodcncf  40592  dvmptmulf  40630  dvmptfprod  40638  dvnprodlem1  40639  dvnprodlem3  40641  stoweidlem16  40710  stoweidlem34  40728  stoweidlem62  40756  dirkercncflem2  40798  fourierdlem12  40813  fourierdlem15  40816  fourierdlem34  40835  fourierdlem50  40850  fourierdlem73  40873  fourierdlem94  40894  fourierdlem112  40912  fourierdlem113  40913  intsaluni  41024  sge0lempt  41104  sge0iunmptlemfi  41107  sge0iunmptlemre  41109  sge0iunmpt  41112  sge0ltfirpmpt2  41120  sge0isummpt2  41126  sge0xaddlem2  41128  sge0xadd  41129  meadjiun  41160  voliunsge0lem  41166  meaiuninclem  41174  meaiunincf  41177  meaiuninc3v  41178  meaiuninc3  41179  meaiininclem  41180  meaiininc  41181  isomennd  41225  ovn0lem  41259  sge0hsphoire  41283  hoidmvlelem1  41289  hoidmvlelem2  41290  hoidmvlelem3  41291  hoidmvlelem5  41293  hspmbllem2  41321  hoimbl2  41359  vonhoire  41366  vonioo  41376  vonicc  41379  vonn0ioo2  41384  vonn0icc2  41386  pimincfltioc  41406  salpreimagtlt  41419  smflimlem4  41462  rexrsb  41680  reuccatpfxs1  42007  sbgoldbm  42245  bgoldbnnsum3prm  42265  tgoldbach  42278  srhmsubc  42642  srhmsubcALTV  42660  cbvmpt2x2  42680
  Copyright terms: Public domain W3C validator