Theorem eleq1w 2817

Description: Weaker version of eleq1 2822 (but more general than elequ1 2120) not depending on ax-ext 2706 nor df-cleq 2726.

Note that this provides a proof of ax-8 2115 from Tarski's FOL and dfclel 2810 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 229), which shows that dfclel 2810 is too powerful to be used as a definition instead of df-clel 2809. (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 2027	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1922	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		dfclel 2810	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		dfclel 2810	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2809

This theorem is referenced by:  clelsb1  2861  cleqh  2863  nfcjust  2882  nfcr  2886  cleqf  2925  rspw  3211  cbvralvw  3212  cbvrexvw  3213  cbvralfw  3274  cbvralsvw  3285  cbvralf  3328  ralcom2  3345  moel  3368  cbvrmovw  3369  cbvreuvw  3370  cbvrmow  3373  cbvreu  3389  cbvrabv  3407  rabrabi  3416  cbvrabw  3432  cbvrabwOLD  3433  nfrab  3436  cbvrab  3437  elrab2w  3648  reu2  3681  reu6  3682  rmo4  3686  reu8  3689  2reu5  3714  ruOLD  3737  csbied  3883  difjust  3901  unjust  3903  injust  3905  dfss2  3917  dfssf  3922  dfdif3OLD  4068  eqeuel  4315  rabeq0w  4337  disj  4400  reldisj  4403  ralidmw  4467  dfif6  4480  rabsnifsb  4677  eluniab  4875  unissb  4894  uniintsn  4938  dfiun2g  4983  dfiunv2  4987  disjxun  5094  cbvmptf  5196  cbvmptfg  5197  cbvmptv  5200  dftr2c  5206  isso2i  5567  dfres2  5998  imai  6031  frpoinsg  6299  tz7.7  6341  fvn0ssdmfun  7017  fmptco  7072  cbvriotaw  7322  cbvriotavw  7323  cbvriota  7326  cbvmpox  7449  cbvmpov  7451  tfis  7795  tfindes  7803  peano5  7833  findes  7840  dfoprab4f  7998  fmpox  8009  xpord2indlem  8087  poseq  8098  soseq  8099  smogt  8297  resixpfo  8872  ixpsnf1o  8874  dom2lem  8927  mapsnend  8971  pw2f1olem  9007  pssnn  9091  ssfi  9095  findcard3  9181  ordiso2  9418  elirrvOLD  9501  cantnflem1d  9595  cantnf  9600  setind  9654  frinsg  9661  tz9.12lem3  9699  infxpen  9922  dfac5lem4  10034  dfac12lem2  10053  kmlem14  10072  cfsmolem  10178  sornom  10185  isf32lem9  10269  axdc2  10357  fpwwe2lem7  10546  fpwwe2  10552  wunex2  10647  dedekindle  11295  wloglei  11667  uzind4s  12819  seqof2  13981  reuccatpfxs1  14668  shftfn  14994  rexuz3  15270  zsum  15639  fsum  15641  sumss  15645  sumss2  15647  fsumcvg2  15648  fsumser  15651  fsumclf  15659  fsumsplitf  15663  isumless  15766  prodfdiv  15817  cbvprod  15834  cbvprodv  15835  zprod  15858  fprod  15862  fprodntriv  15863  prodss  15868  fprod2dlem  15901  fproddivf  15908  fprodsplitf  15909  rpnnen2lem10  16146  cpnnen  16152  sumeven  16312  sumodd  16313  sadcp1  16380  smupp1  16405  pcmptdvds  16820  prmreclem2  16843  prmreclem5  16846  prmreclem6  16847  prmrec  16848  prmdvdsprmo  16968  iscatd2  17602  initoeu2  17938  yoniso  18206  sgrpidmnd  18662  mndind  18751  eqg0subg  19123  symggen  19397  dprd2d2  19973  srhmsubc  20611  isdrngrd  20697  isdrngrdOLD  20699  lbspss  21032  frlmphl  21734  frlmup1  21751  opsrtoslem1  22008  mdetralt  22550  mdetralt2  22551  mdetunilem2  22555  maducoeval2  22582  chfacfscmulgsum  22802  chfacfpmmulgsum  22806  isclo2  23030  neiptopnei  23074  ptcldmpt  23556  elmptrab  23769  hausflimi  23922  hausflim  23923  alexsubALTlem3  23991  alexsubALTlem4  23992  ptcmplem2  23995  cnextcn  24009  cnextfres1  24010  tgphaus  24059  ustuqtop  24188  utopsnneip  24190  ucncn  24226  nrmmetd  24516  xrhmeo  24898  iscau2  25231  caucfil  25237  cmetcaulem  25242  bcth  25283  vitalilem3  25565  vitali  25568  i1f1lem  25644  itg11  25646  i1fres  25660  mbfi1fseq  25676  mbfi1flim  25678  itg2uba  25698  itg2splitlem  25703  isibl2  25721  cbvitg  25731  cbvitgv  25732  itgss3  25770  dvmptfsum  25933  rolle  25948  elply2  26155  plyexmo  26275  lgamgulmlem2  26994  prmorcht  27142  pclogsum  27180  dchr1  27222  lgsdir  27297  lgsdilem2  27298  lgsdi  27299  lgsne0  27300  lgsquadlem3  27347  lgsquad  27348  2sqlem8  27391  nosupcbv  27668  nosupno  27669  nosupdm  27670  nosupbnd1lem1  27674  noinfcbv  27683  noinfno  27684  noinfdm  27685  nocvxminlem  27744  legval  28605  legov  28606  tglineintmo  28663  tglowdim2ln  28672  ishpg  28780  lnopp2hpgb  28784  hpgerlem  28786  colopp  28790  axcontlem1  28986  numedglnl  29166  uvtxnbgrvtx  29415  cusgrres  29471  wspniunwspnon  29945  rusgrnumwwlkb0  29996  frgr3vlem2  30298  3vfriswmgrlem  30301  fusgr2wsp2nb  30358  numclwlk2lem2f1o  30403  lpni  30504  pjhthmo  31326  chscllem2  31662  cbvdisjf  32595  2ndresdju  32676  fmptcof2  32684  aciunf1lem  32689  funcnv4mpt  32696  suppovss  32709  fpwrelmapffslem  32760  fsumiunle  32859  gsumwrd2dccatlem  33108  elrspunsn  33459  1arithufdlem3  33576  fedgmullem1  33735  fldextrspunlsp  33780  extdgfialglem2  33799  zarclssn  33979  esumcvg  34192  fiunelros  34280  measiun  34324  bnj1146  34896  bnj1185  34898  bnj1385  34937  bnj1014  35066  bnj1112  35088  bnj1123  35091  bnj1228  35116  bnj1326  35131  bnj1321  35132  bnj1384  35137  bnj1417  35146  bnj1497  35165  trssfir1om  35216  r1omhfb  35217  fineqvnttrclse  35229  axregscl  35233  setindregs  35235  trssfir1omregs  35241  r1omhfbregs  35242  onvf1odlem2  35247  onvf1odlem3  35248  gonarlem  35537  goalrlem  35539  goalr  35540  mrsubrn  35656  dfon2lem6  35929  dfbigcup2  36040  lineintmo  36300  cbvralvw2  36369  cbvrexvw2  36370  cbvrmovw2  36371  cbvreuvw2  36372  cbvmptvw2  36377  cbvprodvw2  36390  cbvrmodavw  36395  cbvreudavw  36396  cbvrabdavw  36404  cbvmptdavw  36410  cbvriotadavw  36413  cbvixpdavw  36421  cbvproddavw  36423  cbvitgdavw  36424  cbvrabdavw2  36428  cbvmptdavw2  36431  cbvriotadavw2  36433  weiunlem2  36606  eleq2w2ALT  37191  bj-idres  37304  mptsnunlem  37482  ptrest  37759  poimirlem25  37785  mblfinlem2  37798  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  mbfposadd  37807  itg2addnclem  37811  ftc1anclem5  37837  ftc1anclem6  37838  ftc1anclem7  37839  ftc1anc  37841  areacirclem5  37852  fdc1  37886  inxprnres  38430  fsumshftd  39151  pmapglb  39969  polval2N  40105  osumcllem4N  40158  pexmidlem1N  40169  dih1dimatlem  41528  mapdh9a  41988  mapdh9aOLDN  41989  sticksstones2  42340  selvvvval  42770  fsuppind  42775  fphpd  43000  fphpdo  43001  pellex  43019  setindtrs  43209  dford3lem2  43211  fnwe2lem2  43235  mendlmod  43373  cantnfub  43505  tfsconcat0i  43529  rababg  43757  fsovrfovd  44192  fsovcnvlem  44196  scottabf  44423  trfr  45145  elunif  45203  iunincfi  45280  cbvmpo2  45283  cbvmpo1  45284  disjf1  45369  wessf1ornlem  45371  disjinfi  45378  supxrleubrnmptf  45637  monoordxr  45668  monoord2xr  45670  fsummulc1f  45759  fsumnncl  45760  fsumf1of  45762  fsumiunss  45763  fsumreclf  45764  fsumlessf  45765  fsumsermpt  45767  fmulcl  45769  fmul01lt1lem2  45773  fprodexp  45782  fprodabs2  45783  climmulf  45792  climexp  45793  climrecf  45797  climinff  45799  climaddf  45803  mullimc  45804  limcperiod  45816  sumnnodd  45818  neglimc  45833  addlimc  45834  climsubmpt  45846  climreclf  45850  climeldmeqmpt  45854  climfveqmpt  45857  fnlimfvre  45860  climfveqf  45866  climfveqmpt3  45868  climeldmeqf  45869  climeqf  45874  climeldmeqmpt3  45875  climinf2  45893  limsupequz  45909  limsupequzmptf  45917  lmbr3  45933  cnrefiisp  46016  cncfshift  46060  fprodcncf  46086  dvmptmulf  46123  dvmptfprod  46131  dvnprodlem1  46132  dvnprodlem3  46134  stoweidlem16  46202  stoweidlem34  46220  stoweidlem62  46248  dirkercncflem2  46290  fourierdlem12  46305  fourierdlem15  46308  fourierdlem34  46327  fourierdlem50  46342  fourierdlem73  46365  fourierdlem94  46386  fourierdlem112  46404  fourierdlem113  46405  intsaluni  46515  sge0lempt  46596  sge0iunmptlemfi  46599  sge0iunmptlemre  46601  sge0iunmpt  46604  sge0ltfirpmpt2  46612  sge0isummpt2  46618  sge0xaddlem2  46620  sge0xadd  46621  meadjiun  46652  voliunsge0lem  46658  meaiuninclem  46666  meaiunincf  46669  meaiuninc3v  46670  meaiuninc3  46671  meaiininclem  46672  meaiininc  46673  isomennd  46717  ovn0lem  46751  sge0hsphoire  46775  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem3  46783  hoidmvlelem5  46785  hspmbllem2  46813  hoimbl2  46851  vonhoire  46858  vonioo  46868  vonicc  46871  vonn0ioo2  46876  vonn0icc2  46878  pimincfltioc  46902  salpreimagtlt  46916  smflimlem4  46960  ormkglobd  47061  sinnpoly  47079  rexrsb  47288  ichexmpl2  47658  ichnreuop  47660  sbgoldbm  47972  bgoldbnnsum3prm  47992  tgoldbach  48005  srhmsubcALTV  48513  cbvmpox2  48524  mo0sn  49003  f1omoOLD  49081  isthincd2lem1  49612  thincmo  49615  euendfunc  49713