Theorem eleq1w 2819

Description: Weaker version of eleq1 2824 (but more general than elequ1 2121) not depending on ax-ext 2708 nor df-cleq 2728.

Note that this provides a proof of ax-8 2116 from Tarski's FOL and dfclel 2812 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 229), which shows that dfclel 2812 is too powerful to be used as a definition instead of df-clel 2811. (Contributed by BJ, 24-Jun-2019.)

Assertion

Ref	Expression
eleq1w	⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Proof of Theorem eleq1w

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equequ2 2028	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1923	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		dfclel 2812	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		dfclel 2812	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811

This theorem is referenced by:  clelsb1  2863  cleqh  2865  nfcjust  2884  nfcr  2888  cleqf  2927  rspw  3214  cbvralvw  3215  cbvrexvw  3216  cbvralfw  3277  cbvralsvw  3288  cbvralf  3322  ralcom2  3339  moel  3362  cbvrmovw  3363  cbvreuvw  3364  cbvrmow  3367  cbvreu  3381  cbvrabv  3399  rabrabi  3408  cbvrabw  3424  cbvrabwOLD  3425  nfrab  3427  cbvrab  3428  elrab2w  3638  reu2  3671  reu6  3672  rmo4  3676  reu8  3679  2reu5  3704  ruOLD  3727  csbied  3873  difjust  3891  unjust  3893  injust  3895  dfss2  3907  dfssf  3912  dfdif3OLD  4058  eqeuel  4305  rabeq0w  4327  disj  4390  reldisj  4393  ralidmw  4456  dfif6  4469  rabsnifsb  4666  eluniab  4864  unissb  4883  uniintsn  4927  dfiun2g  4972  dfiunv2  4976  disjxun  5083  cbvmptf  5185  cbvmptfg  5186  cbvmptv  5189  dftr2c  5195  isso2i  5576  dfres2  6006  imai  6039  frpoinsg  6307  tz7.7  6349  fvn0ssdmfun  7026  fmptco  7082  cbvriotaw  7333  cbvriotavw  7334  cbvriota  7337  cbvmpox  7460  cbvmpov  7462  tfis  7806  tfindes  7814  peano5  7844  findes  7851  dfoprab4f  8009  fmpox  8020  xpord2indlem  8097  poseq  8108  soseq  8109  smogt  8307  resixpfo  8884  ixpsnf1o  8886  dom2lem  8939  mapsnend  8983  pw2f1olem  9019  pssnn  9103  ssfi  9107  findcard3  9193  ordiso2  9430  elirrvOLD  9513  cantnflem1d  9609  cantnf  9614  setind  9668  frinsg  9675  tz9.12lem3  9713  infxpen  9936  dfac5lem4  10048  dfac12lem2  10067  kmlem14  10086  cfsmolem  10192  sornom  10199  isf32lem9  10283  axdc2  10371  fpwwe2lem7  10560  fpwwe2  10566  wunex2  10661  dedekindle  11310  wloglei  11682  uzind4s  12858  seqof2  14022  reuccatpfxs1  14709  shftfn  15035  rexuz3  15311  zsum  15680  fsum  15682  sumss  15686  sumss2  15688  fsumcvg2  15689  fsumser  15692  fsumclf  15700  fsumsplitf  15704  isumless  15810  prodfdiv  15861  cbvprod  15878  cbvprodv  15879  zprod  15902  fprod  15906  fprodntriv  15907  prodss  15912  fprod2dlem  15945  fproddivf  15952  fprodsplitf  15953  rpnnen2lem10  16190  cpnnen  16196  sumeven  16356  sumodd  16357  sadcp1  16424  smupp1  16449  pcmptdvds  16865  prmreclem2  16888  prmreclem5  16891  prmreclem6  16892  prmrec  16893  prmdvdsprmo  17013  iscatd2  17647  initoeu2  17983  yoniso  18251  sgrpidmnd  18707  mndind  18796  eqg0subg  19171  symggen  19445  dprd2d2  20021  srhmsubc  20657  isdrngrd  20743  isdrngrdOLD  20745  lbspss  21077  frlmphl  21761  frlmup1  21778  opsrtoslem1  22033  mdetralt  22573  mdetralt2  22574  mdetunilem2  22578  maducoeval2  22605  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  isclo2  23053  neiptopnei  23097  ptcldmpt  23579  elmptrab  23792  hausflimi  23945  hausflim  23946  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem2  24018  cnextcn  24032  cnextfres1  24033  tgphaus  24082  ustuqtop  24211  utopsnneip  24213  ucncn  24249  nrmmetd  24539  xrhmeo  24913  iscau2  25244  caucfil  25250  cmetcaulem  25255  bcth  25296  vitalilem3  25577  vitali  25580  i1f1lem  25656  itg11  25658  i1fres  25672  mbfi1fseq  25688  mbfi1flim  25690  itg2uba  25710  itg2splitlem  25715  isibl2  25733  cbvitg  25743  cbvitgv  25744  itgss3  25782  dvmptfsum  25942  rolle  25957  elply2  26161  plyexmo  26279  lgamgulmlem2  26993  prmorcht  27141  pclogsum  27178  dchr1  27220  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  lgsquadlem3  27345  lgsquad  27346  2sqlem8  27389  nosupcbv  27666  nosupno  27667  nosupdm  27668  nosupbnd1lem1  27672  noinfcbv  27681  noinfno  27682  noinfdm  27683  nocvxminlem  27746  legval  28652  legov  28653  tglineintmo  28710  tglowdim2ln  28719  ishpg  28827  lnopp2hpgb  28831  hpgerlem  28833  colopp  28837  axcontlem1  29033  numedglnl  29213  uvtxnbgrvtx  29462  cusgrres  29517  wspniunwspnon  29991  rusgrnumwwlkb0  30042  frgr3vlem2  30344  3vfriswmgrlem  30347  fusgr2wsp2nb  30404  numclwlk2lem2f1o  30449  lpni  30551  pjhthmo  31373  chscllem2  31709  cbvdisjf  32641  2ndresdju  32722  fmptcof2  32730  aciunf1lem  32735  funcnv4mpt  32741  suppovss  32754  fpwrelmapffslem  32805  fsumiunle  32902  gsumwrd2dccatlem  33138  elrspunsn  33489  1arithufdlem3  33606  fedgmullem1  33773  fldextrspunlsp  33818  extdgfialglem2  33837  zarclssn  34017  esumcvg  34230  fiunelros  34318  measiun  34362  bnj1146  34933  bnj1185  34935  bnj1385  34974  bnj1014  35103  bnj1112  35125  bnj1123  35128  bnj1228  35153  bnj1326  35168  bnj1321  35169  bnj1384  35174  bnj1417  35183  bnj1497  35202  trssfir1om  35255  r1omhfb  35256  fineqvnttrclse  35268  axregscl  35272  setindregs  35274  trssfir1omregs  35280  r1omhfbregs  35281  onvf1odlem2  35286  onvf1odlem3  35287  gonarlem  35576  goalrlem  35578  goalr  35579  mrsubrn  35695  dfon2lem6  35968  dfbigcup2  36079  lineintmo  36339  cbvralvw2  36408  cbvrexvw2  36409  cbvrmovw2  36410  cbvreuvw2  36411  cbvmptvw2  36416  cbvprodvw2  36429  cbvrmodavw  36434  cbvreudavw  36435  cbvrabdavw  36443  cbvmptdavw  36449  cbvriotadavw  36452  cbvixpdavw  36460  cbvproddavw  36462  cbvitgdavw  36463  cbvrabdavw2  36467  cbvmptdavw2  36470  cbvriotadavw2  36472  weiunlem  36645  dfttc4  36712  mh-infprim2bi  36729  eleq2w2ALT  37354  bj-idres  37474  mptsnunlem  37654  wl-dfcleq  37830  wl-dfclel  37831  ptrest  37940  poimirlem25  37966  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  mbfposadd  37988  itg2addnclem  37992  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anc  38022  areacirclem5  38033  fdc1  38067  inxprnres  38619  fsumshftd  39398  pmapglb  40216  polval2N  40352  osumcllem4N  40405  pexmidlem1N  40416  dih1dimatlem  41775  mapdh9a  42235  mapdh9aOLDN  42236  sticksstones2  42586  selvvvval  43018  fsuppind  43023  fphpd  43244  fphpdo  43245  pellex  43263  setindtrs  43453  dford3lem2  43455  fnwe2lem2  43479  mendlmod  43617  cantnfub  43749  tfsconcat0i  43773  rababg  44001  fsovrfovd  44436  fsovcnvlem  44440  scottabf  44667  trfr  45389  elunif  45447  iunincfi  45524  cbvmpo2  45527  cbvmpo1  45528  disjf1  45613  wessf1ornlem  45615  disjinfi  45622  supxrleubrnmptf  45879  monoordxr  45910  monoord2xr  45912  fsummulc1f  46001  fsumnncl  46002  fsumf1of  46004  fsumiunss  46005  fsumreclf  46006  fsumlessf  46007  fsumsermpt  46009  fmulcl  46011  fmul01lt1lem2  46015  fprodexp  46024  fprodabs2  46025  climmulf  46034  climexp  46035  climrecf  46039  climinff  46041  climaddf  46045  mullimc  46046  limcperiod  46058  sumnnodd  46060  neglimc  46075  addlimc  46076  climsubmpt  46088  climreclf  46092  climeldmeqmpt  46096  climfveqmpt  46099  fnlimfvre  46102  climfveqf  46108  climfveqmpt3  46110  climeldmeqf  46111  climeqf  46116  climeldmeqmpt3  46117  climinf2  46135  limsupequz  46151  limsupequzmptf  46159  lmbr3  46175  cnrefiisp  46258  cncfshift  46302  fprodcncf  46328  dvmptmulf  46365  dvmptfprod  46373  dvnprodlem1  46374  dvnprodlem3  46376  stoweidlem16  46444  stoweidlem34  46462  stoweidlem62  46490  dirkercncflem2  46532  fourierdlem12  46547  fourierdlem15  46550  fourierdlem34  46569  fourierdlem50  46584  fourierdlem73  46607  fourierdlem94  46628  fourierdlem112  46646  fourierdlem113  46647  intsaluni  46757  sge0lempt  46838  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isummpt2  46860  sge0xaddlem2  46862  sge0xadd  46863  meadjiun  46894  voliunsge0lem  46900  meaiuninclem  46908  meaiunincf  46911  meaiuninc3v  46912  meaiuninc3  46913  meaiininclem  46914  meaiininc  46915  isomennd  46959  ovn0lem  46993  sge0hsphoire  47017  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem5  47027  hspmbllem2  47055  hoimbl2  47093  vonhoire  47100  vonioo  47110  vonicc  47113  vonn0ioo2  47118  vonn0icc2  47120  pimincfltioc  47144  salpreimagtlt  47158  smflimlem4  47202  ormkglobd  47305  sinnpoly  47339  rexrsb  47548  ichexmpl2  47930  ichnreuop  47932  sbgoldbm  48260  bgoldbnnsum3prm  48280  tgoldbach  48293  srhmsubcALTV  48801  cbvmpox2  48812  mo0sn  49291  f1omoOLD  49369  isthincd2lem1  49900  thincmo  49903  euendfunc  50001