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

Theorem eleq1w 2833
Description: Weaker version of eleq1 2838 (but more general than elequ1 2152) not depending on ax-ext 2751 nor df-cleq 2764. (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 2111 . . . 4 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
21anbi1d 615 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝑥𝑧𝐴) ↔ (𝑧 = 𝑦𝑧𝐴)))
32exbidv 2002 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥𝑧𝐴) ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴)))
4 df-clel 2767 . 2 (𝑥𝐴 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝐴))
5 df-clel 2767 . 2 (𝑦𝐴 ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴))
63, 4, 53bitr4g 303 1 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wex 1852  wcel 2145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-clel 2767
This theorem is referenced by:  cleqh  2873  clelsb3  2878  nfcjust  2901  clelsb3f  2917  ralcom2  3252  nfrab  3272  cbvralf  3314  cbvreu  3318  cbvrab  3348  ralab2  3523  rexab2  3525  reu2  3546  reu6  3547  rmo4  3551  reu8  3554  2reu5  3568  ru  3586  difjust  3725  unjust  3727  injust  3729  dfss2f  3743  dfdif3  3871  eqeuel  4088  rabsnifsb  4393  eluniab  4585  elintab  4622  uniintsn  4648  dfiunv2  4690  disjxun  4784  cbvmptf  4882  cbvmpt  4883  isso2i  5202  dfres2  5594  imai  5619  wfisg  5858  tz7.7  5892  fvn0ssdmfun  6493  fmptco  6539  cbvriota  6764  cbvmpt2x  6880  tfis  7201  tfindes  7209  findes  7243  resiexg  7249  dfoprab4f  7375  fmpt2x  7386  wfrlem10  7577  smogt  7617  resixpfo  8100  ixpsnf1o  8102  dom2lem  8149  mapsnend  8188  pw2f1olem  8220  findcard3  8359  ordiso2  8576  elirrv  8657  cantnflem1d  8749  cantnf  8754  setind  8774  tz9.12lem3  8816  infxpen  9037  aceq1  9140  aceq2  9142  dfac12lem2  9168  kmlem4  9177  kmlem14  9187  cfsmolem  9294  sornom  9301  isf32lem9  9385  axdc2  9473  fpwwe2lem8  9661  fpwwe2  9667  wunex2  9762  dedekindle  10403  wloglei  10762  uzind4s  11950  seqof2  13066  reuccats1  13689  shftfn  14021  rexuz3  14296  zsum  14657  fsum  14659  sumss  14663  sumss2  14665  fsumcvg2  14666  fsumser  14669  fsumsplitf  14680  isumless  14784  prodfdiv  14835  cbvprod  14852  zprod  14874  fprod  14878  fprodntriv  14879  prodss  14884  fprod2dlem  14917  fproddivf  14924  fprodsplitf  14925  rpnnen2lem10  15158  cpnnen  15164  sumeven  15318  sumodd  15319  sadcp1  15385  smupp1  15410  pcmptdvds  15805  prmreclem2  15828  prmreclem5  15831  prmreclem6  15832  prmrec  15833  prmdvdsprmo  15953  iscatd2  16549  initoeu2  16873  yoniso  17133  mrcmndind  17574  symggen  18097  dprd2d2  18651  isdrngrd  18983  lbspss  19295  opsrtoslem1  19699  frlmphl  20337  frlmup1  20354  mdetralt  20632  mdetralt2  20633  mdetunilem2  20637  maducoeval2  20664  chfacfscmulgsum  20885  chfacfpmmulgsum  20889  isclo2  21113  neiptopnei  21157  ptcldmpt  21638  elmptrab  21851  hausflimi  22004  hausflim  22005  alexsubALTlem3  22073  alexsubALTlem4  22074  ptcmplem2  22077  cnextcn  22091  cnextfres1  22092  tgphaus  22140  ustuqtop  22270  utopsnneip  22272  ucncn  22309  nrmmetd  22599  xrhmeo  22965  iscau2  23294  caucfil  23300  cmetcaulem  23305  bcth  23345  vitalilem3  23598  vitali  23601  i1f1lem  23676  itg11  23678  i1fres  23692  mbfi1fseq  23708  mbfi1flim  23710  itg2uba  23730  itg2splitlem  23735  isibl2  23753  cbvitg  23762  itgss3  23801  dvmptfsum  23958  rolle  23973  elply2  24172  plyexmo  24288  lgamgulmlem2  24977  prmorcht  25125  pclogsum  25161  dchr1  25203  lgsdir  25278  lgsdilem2  25279  lgsdi  25280  lgsne0  25281  lgsquadlem3  25328  lgsquad  25329  2sqlem8  25372  legval  25700  legov  25701  tglineintmo  25758  tglowdim2ln  25767  ishpg  25872  lnopp2hpgb  25876  hpgerlem  25878  colopp  25882  axcontlem1  26065  numedglnl  26261  uvtxnbgrvtx  26520  cusgrres  26579  wspniunwspnon  27070  rusgrnumwwlkb0  27120  frgr3vlem2  27456  3vfriswmgrlem  27459  fusgr2wsp2nb  27516  numclwlk2lem2f1o  27570  numclwlk2lem2f1oOLD  27577  lpni  27674  pjhthmo  28501  chscllem2  28837  moel  29663  cbvdisjf  29723  fmptcof2  29797  aciunf1lem  29802  funcnv4mpt  29810  fpwrelmapffslem  29847  fsumiunle  29915  esumcvg  30488  fiunelros  30577  measiun  30621  bnj1146  31200  bnj1185  31202  bnj1385  31241  bnj1014  31368  bnj1112  31389  bnj1123  31392  bnj1228  31417  bnj1326  31432  bnj1321  31433  bnj1384  31438  bnj1417  31447  bnj1497  31466  mrsubrn  31748  dfon2lem6  32029  frpoinsg  32078  frinsg  32082  poseq  32090  soseq  32091  nosupno  32186  nosupdm  32187  nosupbnd1lem1  32191  noeta  32205  nocvxminlem  32230  dfbigcup2  32343  lineintmo  32601  bj-nfcjust  33182  mptsnunlem  33522  ptrest  33741  poimirlem25  33767  mblfinlem2  33780  mblfinlem3  33781  mblfinlem4  33782  ismblfin  33783  mbfposadd  33789  itg2addnclem  33793  ftc1anclem5  33821  ftc1anclem6  33822  ftc1anclem7  33823  ftc1anc  33825  areacirclem5  33836  fdc1  33874  inxprnres  34403  prtlem13  34676  prtlem16  34677  fsumshftd  34760  pmapglb  35578  polval2N  35714  osumcllem4N  35767  pexmidlem1N  35778  dih1dimatlem  37139  mapdh9a  37599  mapdh9aOLDN  37600  fphpd  37906  fphpdo  37907  pellex  37925  setindtrs  38118  dford3lem2  38120  fnwe2lem2  38147  mendlmod  38289  rababg  38405  fsovrfovd  38829  fsovcnvlem  38833  elunif  39697  iunincfi  39793  cbvmpt22  39798  cbvmpt21  39799  disjf1  39889  wessf1ornlem  39891  disjinfi  39900  supxrleubrnmptf  40196  monoordxr  40229  monoord2xr  40231  fsumclf  40319  fsummulc1f  40320  fsumnncl  40321  fsumf1of  40324  fsumiunss  40325  fsumreclf  40326  fsumlessf  40327  fsumsermpt  40329  fmulcl  40331  fmul01lt1lem2  40335  fprodexp  40344  fprodabs2  40345  climmulf  40354  climexp  40355  climrecf  40359  climinff  40361  climaddf  40365  mullimc  40366  limcperiod  40378  sumnnodd  40380  neglimc  40397  addlimc  40398  climsubmpt  40410  climreclf  40414  climeldmeqmpt  40418  climfveqmpt  40421  fnlimfvre  40424  climfveqf  40430  climfveqmpt3  40432  climeldmeqf  40433  climeqf  40438  climeldmeqmpt3  40439  climinf2  40457  limsupequz  40473  limsupequzmptf  40481  lmbr3  40497  cnrefiisp  40574  cncfshift  40605  fprodcncf  40632  dvmptmulf  40670  dvmptfprod  40678  dvnprodlem1  40679  dvnprodlem3  40681  stoweidlem16  40750  stoweidlem34  40768  stoweidlem62  40796  dirkercncflem2  40838  fourierdlem12  40853  fourierdlem15  40856  fourierdlem34  40875  fourierdlem50  40890  fourierdlem73  40913  fourierdlem94  40934  fourierdlem112  40952  fourierdlem113  40953  intsaluni  41064  sge0lempt  41144  sge0iunmptlemfi  41147  sge0iunmptlemre  41149  sge0iunmpt  41152  sge0ltfirpmpt2  41160  sge0isummpt2  41166  sge0xaddlem2  41168  sge0xadd  41169  meadjiun  41200  voliunsge0lem  41206  meaiuninclem  41214  meaiunincf  41217  meaiuninc3v  41218  meaiuninc3  41219  meaiininclem  41220  meaiininc  41221  isomennd  41265  ovn0lem  41299  sge0hsphoire  41323  hoidmvlelem1  41329  hoidmvlelem2  41330  hoidmvlelem3  41331  hoidmvlelem5  41333  hspmbllem2  41361  hoimbl2  41399  vonhoire  41406  vonioo  41416  vonicc  41419  vonn0ioo2  41424  vonn0icc2  41426  pimincfltioc  41446  salpreimagtlt  41459  smflimlem4  41502  rexrsb  41689  reuccatpfxs1  41962  sbgoldbm  42200  bgoldbnnsum3prm  42220  tgoldbach  42233  srhmsubc  42604  srhmsubcALTV  42622  cbvmpt2x2  42642
  Copyright terms: Public domain W3C validator