Theorem eleq1w 2867

Description: Weaker version of eleq1 2872 (but more general than elequ1 2090) not depending on ax-ext 2771 nor df-cleq 2790.

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∃wex 1765   ∈ wcel 2083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-clel 2865

This theorem is referenced by:  cleqh  2908  clelsb3  2912  clelsb3vOLD  2913  nfcjust  2936  clelsb3fOLD  2956  cleqf  2980  ralcom2  3326  nfrab  3347  cbvralf  3399  cbvreu  3403  cbvrab  3436  cbvrabv  3437  ralab2OLD  3630  rexab2OLD  3633  reu2  3655  reu6  3656  rmo4  3660  reu8  3663  2reu5  3688  ru  3710  difjust  3867  unjust  3869  injust  3871  dfss2f  3886  dfdif3  4018  eqeuel  4248  rabsnifsb  4571  eluniab  4762  elintab  4799  uniintsn  4825  dfiunv2  4869  disjxun  4966  cbvmptf  5066  cbvmpt  5067  isso2i  5403  dfres2  5797  imai  5825  wfisg  6065  tz7.7  6099  fvn0ssdmfun  6714  fmptco  6761  cbvriota  6994  cbvmpox  7110  tfis  7432  tfindes  7440  findes  7475  dfoprab4f  7617  fmpox  7628  wfrlem10  7823  smogt  7863  resixpfo  8355  ixpsnf1o  8357  dom2lem  8404  mapsnend  8443  pw2f1olem  8475  findcard3  8614  ordiso2  8832  elirrv  8913  cantnflem1d  9004  cantnf  9009  setind  9029  tz9.12lem3  9071  infxpen  9293  dfac12lem2  9423  kmlem14  9442  cfsmolem  9545  sornom  9552  isf32lem9  9636  axdc2  9724  fpwwe2lem8  9912  fpwwe2  9918  wunex2  10013  dedekindle  10657  wloglei  11026  uzind4s  12161  seqof2  13282  reuccatpfxs1  13949  shftfn  14270  rexuz3  14546  zsum  14912  fsum  14914  sumss  14918  sumss2  14920  fsumcvg2  14921  fsumser  14924  fsumsplitf  14935  isumless  15037  prodfdiv  15089  cbvprod  15106  zprod  15128  fprod  15132  fprodntriv  15133  prodss  15138  fprod2dlem  15171  fproddivf  15178  fprodsplitf  15179  rpnnen2lem10  15413  cpnnen  15419  sumeven  15575  sumodd  15576  sadcp1  15641  smupp1  15666  pcmptdvds  16063  prmreclem2  16086  prmreclem5  16089  prmreclem6  16090  prmrec  16091  prmdvdsprmo  16211  iscatd2  16785  initoeu2  17109  yoniso  17368  mndind  17809  symggen  18333  dprd2d2  18887  isdrngrd  19222  lbspss  19548  opsrtoslem1  19955  frlmphl  20611  frlmup1  20628  mdetralt  20905  mdetralt2  20906  mdetunilem2  20910  maducoeval2  20937  chfacfscmulgsum  21156  chfacfpmmulgsum  21160  isclo2  21384  neiptopnei  21428  ptcldmpt  21910  elmptrab  22123  hausflimi  22276  hausflim  22277  alexsubALTlem3  22345  alexsubALTlem4  22346  ptcmplem2  22349  cnextcn  22363  cnextfres1  22364  tgphaus  22412  ustuqtop  22542  utopsnneip  22544  ucncn  22581  nrmmetd  22871  xrhmeo  23237  iscau2  23567  caucfil  23573  cmetcaulem  23578  bcth  23619  vitalilem3  23898  vitali  23901  i1f1lem  23977  itg11  23979  i1fres  23993  mbfi1fseq  24009  mbfi1flim  24011  itg2uba  24031  itg2splitlem  24036  isibl2  24054  cbvitg  24063  itgss3  24102  dvmptfsum  24259  rolle  24274  elply2  24473  plyexmo  24589  lgamgulmlem2  25293  prmorcht  25441  pclogsum  25477  dchr1  25519  lgsdir  25594  lgsdilem2  25595  lgsdi  25596  lgsne0  25597  lgsquadlem3  25644  lgsquad  25645  2sqlem8  25688  legval  26056  legov  26057  tglineintmo  26114  tglowdim2ln  26123  ishpg  26231  lnopp2hpgb  26235  hpgerlem  26237  colopp  26241  axcontlem1  26437  numedglnl  26616  uvtxnbgrvtx  26862  cusgrres  26917  wspniunwspnon  27388  rusgrnumwwlkb0  27436  frgr3vlem2  27741  3vfriswmgrlem  27744  fusgr2wsp2nb  27801  numclwlk2lem2f1o  27846  lpni  27944  pjhthmo  28766  chscllem2  29102  moel  29940  cbvdisjf  30007  fmptcof2  30088  aciunf1lem  30093  funcnv4mpt  30100  suppovss  30112  fpwrelmapffslem  30152  fsumiunle  30225  fedgmullem1  30625  esumcvg  30958  fiunelros  31046  measiun  31090  bnj1146  31676  bnj1185  31678  bnj1385  31717  bnj1014  31844  bnj1112  31865  bnj1123  31868  bnj1228  31893  bnj1326  31908  bnj1321  31909  bnj1384  31914  bnj1417  31923  bnj1497  31942  gonarlem  32251  goalrlem  32253  goalr  32254  mrsubrn  32370  dfon2lem6  32643  frpoinsg  32692  frinsg  32698  poseq  32706  soseq  32707  nosupno  32814  nosupdm  32815  nosupbnd1lem1  32819  noeta  32833  nocvxminlem  32858  dfbigcup2  32971  lineintmo  33229  mptsnunlem  34171  wl-dfralflem  34390  ptrest  34443  poimirlem25  34469  mblfinlem2  34482  mblfinlem3  34483  mblfinlem4  34484  ismblfin  34485  mbfposadd  34491  itg2addnclem  34495  ftc1anclem5  34523  ftc1anclem6  34524  ftc1anclem7  34525  ftc1anc  34527  areacirclem5  34538  fdc1  34574  inxprnres  35102  fsumshftd  35640  pmapglb  36458  polval2N  36594  osumcllem4N  36647  pexmidlem1N  36658  dih1dimatlem  38017  mapdh9a  38477  mapdh9aOLDN  38478  fphpd  38919  fphpdo  38920  pellex  38938  setindtrs  39128  dford3lem2  39130  fnwe2lem2  39157  mendlmod  39299  rababg  39439  fsovrfovd  39861  fsovcnvlem  39865  scottabf  40094  elunif  40833  iunincfi  40920  cbvmpo2  40923  cbvmpo1  40924  disjf1  41004  wessf1ornlem  41006  disjinfi  41015  supxrleubrnmptf  41290  monoordxr  41322  monoord2xr  41324  fsumclf  41413  fsummulc1f  41414  fsumnncl  41415  fsumf1of  41418  fsumiunss  41419  fsumreclf  41420  fsumlessf  41421  fsumsermpt  41423  fmulcl  41425  fmul01lt1lem2  41429  fprodexp  41438  fprodabs2  41439  climmulf  41448  climexp  41449  climrecf  41453  climinff  41455  climaddf  41459  mullimc  41460  limcperiod  41472  sumnnodd  41474  neglimc  41491  addlimc  41492  climsubmpt  41504  climreclf  41508  climeldmeqmpt  41512  climfveqmpt  41515  fnlimfvre  41518  climfveqf  41524  climfveqmpt3  41526  climeldmeqf  41527  climeqf  41532  climeldmeqmpt3  41533  climinf2  41551  limsupequz  41567  limsupequzmptf  41575  lmbr3  41591  cnrefiisp  41674  cncfshift  41720  fprodcncf  41747  dvmptmulf  41785  dvmptfprod  41793  dvnprodlem1  41794  dvnprodlem3  41796  stoweidlem16  41865  stoweidlem34  41883  stoweidlem62  41911  dirkercncflem2  41953  fourierdlem12  41968  fourierdlem15  41971  fourierdlem34  41990  fourierdlem50  42005  fourierdlem73  42028  fourierdlem94  42049  fourierdlem112  42067  fourierdlem113  42068  intsaluni  42176  sge0lempt  42256  sge0iunmptlemfi  42259  sge0iunmptlemre  42261  sge0iunmpt  42264  sge0ltfirpmpt2  42272  sge0isummpt2  42278  sge0xaddlem2  42280  sge0xadd  42281  meadjiun  42312  voliunsge0lem  42318  meaiuninclem  42326  meaiunincf  42329  meaiuninc3v  42330  meaiuninc3  42331  meaiininclem  42332  meaiininc  42333  isomennd  42377  ovn0lem  42411  sge0hsphoire  42435  hoidmvlelem1  42441  hoidmvlelem2  42442  hoidmvlelem3  42443  hoidmvlelem5  42445  hspmbllem2  42473  hoimbl2  42511  vonhoire  42518  vonioo  42528  vonicc  42531  vonn0ioo2  42536  vonn0icc2  42538  pimincfltioc  42558  salpreimagtlt  42571  smflimlem4  42614  rexrsb  42836  ichexmpl2  43136  ichnreuop  43138  sbgoldbm  43453  bgoldbnnsum3prm  43473  tgoldbach  43486  srhmsubc  43847  srhmsubcALTV  43865  cbvmpox2  43884