Theorem eleq1w 2811

Description: Weaker version of eleq1 2816 (but more general than elequ1 2116) not depending on ax-ext 2701 nor df-cleq 2721.

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803

This theorem is referenced by:  clelsb1  2855  cleqh  2857  nfcjust  2877  nfcr  2881  cleqf  2920  rspw  3206  cbvralvw  3207  cbvrexvw  3208  cbvralfw  3269  cbvralsvw  3280  cbvralf  3323  ralcom2  3340  moel  3365  cbvrmovw  3366  cbvreuvw  3367  cbvrmow  3370  cbvreu  3386  cbvrabv  3405  rabrabi  3414  cbvrabw  3430  cbvrabwOLD  3431  nfrab  3434  cbvrab  3435  elrab2w  3652  reu2  3685  reu6  3686  rmo4  3690  reu8  3693  2reu5  3718  ruOLD  3741  csbied  3887  difjust  3905  unjust  3907  injust  3909  dfss2  3921  dfssf  3926  dfdif3OLD  4069  eqeuel  4316  rabeq0w  4338  disj  4401  reldisj  4404  ralidmw  4459  dfif6  4479  rabsnifsb  4674  eluniab  4872  unissb  4890  elintabOLD  4909  uniintsn  4935  dfiun2g  4980  dfiunv2  4984  disjxun  5090  cbvmptf  5192  cbvmptfg  5193  cbvmptv  5196  dftr2c  5202  isso2i  5564  dfres2  5992  imai  6025  frpoinsg  6291  tz7.7  6333  fvn0ssdmfun  7008  fmptco  7063  cbvriotaw  7315  cbvriotavw  7316  cbvriota  7319  cbvmpox  7442  cbvmpov  7444  tfis  7788  tfindes  7796  peano5  7826  findes  7833  dfoprab4f  7991  fmpox  8002  xpord2indlem  8080  poseq  8091  soseq  8092  smogt  8290  resixpfo  8863  ixpsnf1o  8865  dom2lem  8917  mapsnend  8961  pw2f1olem  8998  pssnn  9082  ssfi  9087  findcard3  9172  ordiso2  9407  elirrvOLD  9490  cantnflem1d  9584  cantnf  9589  setind  9630  frinsg  9647  tz9.12lem3  9685  infxpen  9908  dfac5lem4  10020  dfac12lem2  10039  kmlem14  10058  cfsmolem  10164  sornom  10171  isf32lem9  10255  axdc2  10343  fpwwe2lem7  10531  fpwwe2  10537  wunex2  10632  dedekindle  11280  wloglei  11652  uzind4s  12809  seqof2  13967  reuccatpfxs1  14653  shftfn  14980  rexuz3  15256  zsum  15625  fsum  15627  sumss  15631  sumss2  15633  fsumcvg2  15634  fsumser  15637  fsumclf  15645  fsumsplitf  15649  isumless  15752  prodfdiv  15803  cbvprod  15820  cbvprodv  15821  zprod  15844  fprod  15848  fprodntriv  15849  prodss  15854  fprod2dlem  15887  fproddivf  15894  fprodsplitf  15895  rpnnen2lem10  16132  cpnnen  16138  sumeven  16298  sumodd  16299  sadcp1  16366  smupp1  16391  pcmptdvds  16806  prmreclem2  16829  prmreclem5  16832  prmreclem6  16833  prmrec  16834  prmdvdsprmo  16954  iscatd2  17587  initoeu2  17923  yoniso  18191  sgrpidmnd  18613  mndind  18702  eqg0subg  19075  symggen  19349  dprd2d2  19925  srhmsubc  20565  isdrngrd  20651  isdrngrdOLD  20653  lbspss  20986  frlmphl  21688  frlmup1  21705  opsrtoslem1  21960  mdetralt  22493  mdetralt2  22494  mdetunilem2  22498  maducoeval2  22525  chfacfscmulgsum  22745  chfacfpmmulgsum  22749  isclo2  22973  neiptopnei  23017  ptcldmpt  23499  elmptrab  23712  hausflimi  23865  hausflim  23866  alexsubALTlem3  23934  alexsubALTlem4  23935  ptcmplem2  23938  cnextcn  23952  cnextfres1  23953  tgphaus  24002  ustuqtop  24132  utopsnneip  24134  ucncn  24170  nrmmetd  24460  xrhmeo  24842  iscau2  25175  caucfil  25181  cmetcaulem  25186  bcth  25227  vitalilem3  25509  vitali  25512  i1f1lem  25588  itg11  25590  i1fres  25604  mbfi1fseq  25620  mbfi1flim  25622  itg2uba  25642  itg2splitlem  25647  isibl2  25665  cbvitg  25675  cbvitgv  25676  itgss3  25714  dvmptfsum  25877  rolle  25892  elply2  26099  plyexmo  26219  lgamgulmlem2  26938  prmorcht  27086  pclogsum  27124  dchr1  27166  lgsdir  27241  lgsdilem2  27242  lgsdi  27243  lgsne0  27244  lgsquadlem3  27291  lgsquad  27292  2sqlem8  27335  nosupcbv  27612  nosupno  27613  nosupdm  27614  nosupbnd1lem1  27618  noinfcbv  27627  noinfno  27628  noinfdm  27629  nocvxminlem  27688  legval  28529  legov  28530  tglineintmo  28587  tglowdim2ln  28596  ishpg  28704  lnopp2hpgb  28708  hpgerlem  28710  colopp  28714  axcontlem1  28909  numedglnl  29089  uvtxnbgrvtx  29338  cusgrres  29394  wspniunwspnon  29868  rusgrnumwwlkb0  29916  frgr3vlem2  30218  3vfriswmgrlem  30221  fusgr2wsp2nb  30278  numclwlk2lem2f1o  30323  lpni  30424  pjhthmo  31246  chscllem2  31582  cbvdisjf  32515  2ndresdju  32592  fmptcof2  32600  aciunf1lem  32605  funcnv4mpt  32612  suppovss  32623  fpwrelmapffslem  32675  fsumiunle  32774  gsumwrd2dccatlem  33019  elrspunsn  33366  1arithufdlem3  33483  fedgmullem1  33596  fldextrspunlsp  33641  extdgfialglem2  33660  zarclssn  33840  esumcvg  34053  fiunelros  34141  measiun  34185  bnj1146  34758  bnj1185  34760  bnj1385  34799  bnj1014  34928  bnj1112  34950  bnj1123  34953  bnj1228  34978  bnj1326  34993  bnj1321  34994  bnj1384  34999  bnj1417  35008  bnj1497  35027  axregscl  35063  setindregs  35065  onvf1odlem2  35077  onvf1odlem3  35078  gonarlem  35367  goalrlem  35369  goalr  35370  mrsubrn  35486  dfon2lem6  35762  dfbigcup2  35873  lineintmo  36131  cbvralvw2  36200  cbvrexvw2  36201  cbvrmovw2  36202  cbvreuvw2  36203  cbvmptvw2  36208  cbvprodvw2  36221  cbvrmodavw  36226  cbvreudavw  36227  cbvrabdavw  36235  cbvmptdavw  36241  cbvriotadavw  36244  cbvixpdavw  36252  cbvproddavw  36254  cbvitgdavw  36255  cbvrabdavw2  36259  cbvmptdavw2  36262  cbvriotadavw2  36264  weiunlem2  36437  eleq2w2ALT  37021  bj-idres  37134  mptsnunlem  37312  ptrest  37599  poimirlem25  37625  mblfinlem2  37638  mblfinlem3  37639  mblfinlem4  37640  ismblfin  37641  mbfposadd  37647  itg2addnclem  37651  ftc1anclem5  37677  ftc1anclem6  37678  ftc1anclem7  37679  ftc1anc  37681  areacirclem5  37692  fdc1  37726  inxprnres  38266  fsumshftd  38931  pmapglb  39749  polval2N  39885  osumcllem4N  39938  pexmidlem1N  39949  dih1dimatlem  41308  mapdh9a  41768  mapdh9aOLDN  41769  sticksstones2  42120  selvvvval  42558  fsuppind  42563  fphpd  42789  fphpdo  42790  pellex  42808  setindtrs  42998  dford3lem2  43000  fnwe2lem2  43024  mendlmod  43162  cantnfub  43294  tfsconcat0i  43318  rababg  43547  fsovrfovd  43982  fsovcnvlem  43986  scottabf  44213  trfr  44936  elunif  44994  iunincfi  45072  cbvmpo2  45075  cbvmpo1  45076  disjf1  45161  wessf1ornlem  45163  disjinfi  45170  supxrleubrnmptf  45430  monoordxr  45461  monoord2xr  45463  fsummulc1f  45552  fsumnncl  45553  fsumf1of  45555  fsumiunss  45556  fsumreclf  45557  fsumlessf  45558  fsumsermpt  45560  fmulcl  45562  fmul01lt1lem2  45566  fprodexp  45575  fprodabs2  45576  climmulf  45585  climexp  45586  climrecf  45590  climinff  45592  climaddf  45596  mullimc  45597  limcperiod  45609  sumnnodd  45611  neglimc  45628  addlimc  45629  climsubmpt  45641  climreclf  45645  climeldmeqmpt  45649  climfveqmpt  45652  fnlimfvre  45655  climfveqf  45661  climfveqmpt3  45663  climeldmeqf  45664  climeqf  45669  climeldmeqmpt3  45670  climinf2  45688  limsupequz  45704  limsupequzmptf  45712  lmbr3  45728  cnrefiisp  45811  cncfshift  45855  fprodcncf  45881  dvmptmulf  45918  dvmptfprod  45926  dvnprodlem1  45927  dvnprodlem3  45929  stoweidlem16  45997  stoweidlem34  46015  stoweidlem62  46043  dirkercncflem2  46085  fourierdlem12  46100  fourierdlem15  46103  fourierdlem34  46122  fourierdlem50  46137  fourierdlem73  46160  fourierdlem94  46181  fourierdlem112  46199  fourierdlem113  46200  intsaluni  46310  sge0lempt  46391  sge0iunmptlemfi  46394  sge0iunmptlemre  46396  sge0iunmpt  46399  sge0ltfirpmpt2  46407  sge0isummpt2  46413  sge0xaddlem2  46415  sge0xadd  46416  meadjiun  46447  voliunsge0lem  46453  meaiuninclem  46461  meaiunincf  46464  meaiuninc3v  46465  meaiuninc3  46466  meaiininclem  46467  meaiininc  46468  isomennd  46512  ovn0lem  46546  sge0hsphoire  46570  hoidmvlelem1  46576  hoidmvlelem2  46577  hoidmvlelem3  46578  hoidmvlelem5  46580  hspmbllem2  46608  hoimbl2  46646  vonhoire  46653  vonioo  46663  vonicc  46666  vonn0ioo2  46671  vonn0icc2  46673  pimincfltioc  46697  salpreimagtlt  46711  smflimlem4  46755  ormkglobd  46856  sinnpoly  46875  rexrsb  47084  ichexmpl2  47454  ichnreuop  47456  sbgoldbm  47768  bgoldbnnsum3prm  47788  tgoldbach  47801  srhmsubcALTV  48309  cbvmpox2  48320  mo0sn  48800  f1omoOLD  48878  isthincd2lem1  49410  thincmo  49413  euendfunc  49511