Theorem eleq1w 2852

Description: Weaker version of eleq1 2857 (but more general than elequ1 2156) not depending on ax-ext 2741 nor df-cleq 2761.

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∃wex 1806   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844

This theorem is referenced by:  clelsb1  2896  cleqh  2898  nfcjust  2917  nfcr  2921  cleqf  2959  rspw  3248  cbvralvw  3249  cbvrexvw  3250  cbvralfw  3311  cbvralsvw  3322  cbvralf  3356  ralcom2  3373  moel  3396  cbvrmovw  3397  cbvreuvw  3398  cbvrmow  3401  cbvreu  3415  cbvrabv  3433  rabrabi  3442  cbvrabw  3458  cbvrabwOLD  3459  nfrab  3461  cbvrab  3462  elrab2w  3664  reu2  3697  reu6  3698  rmo4  3702  reu8  3705  2reu5  3730  csbied  3897  difjust  3915  unjust  3917  injust  3919  dfss2  3931  dfssf  3936  dfdif3OLD  4081  eqeuel  4328  rabeq0w  4351  disj  4416  reldisj  4419  ralidmw  4482  dfif6  4495  rabsnifsb  4693  eluniab  4890  unissb  4910  uniintsn  4954  dfiun2g  4998  dfiunv2  5002  disjxun  5111  cbvmptf  5215  cbvmptfg  5216  cbvmptv  5219  dftr2c  5225  isso2i  5607  dfres2  6044  imai  6077  frpoinsg  6345  tz7.7  6387  fvn0ssdmfun  7070  fmptco  7126  cbvriotaw  7377  cbvriotavw  7378  cbvriota  7381  cbvmpox  7504  cbvmpov  7506  tfis  7850  tfindes  7858  peano5  7889  findes  7896  dfoprab4f  8052  fmpox  8063  xpord2indlem  8142  poseq  8153  soseq  8154  smogt  8353  resixpfo  8933  ixpsnf1o  8935  dom2lem  8988  mapsnend  9032  pw2f1olem  9068  pssnn  9152  ssfi  9156  findcard3  9242  ordiso2  9476  elirrvOLDOLD  9560  cantnflem1d  9656  cantnf  9661  setind  9715  frinsg  9722  tz9.12lem3  9760  scottabf  9865  infxpen  9997  dfac5lem4  10109  dfac12lem2  10127  kmlem14  10146  cfsmolem  10253  sornom  10260  isf32lem9  10344  axdc2  10432  fpwwe2lem7  10621  fpwwe2  10627  wunex2  10722  dedekindle  11373  wloglei  11745  uzind4s  12931  seqof2  14095  reuccatpfxs1  14783  shftfn  15109  rexuz3  15399  zsum  15768  fsum  15770  sumss  15774  sumss2  15776  fsumcvg2  15777  fsumser  15780  fsumclf  15788  fsumsplitf  15792  isumless  15898  prodfdiv  15949  cbvprod  15966  cbvprodv  15967  zprod  15990  fprod  15994  fprodntriv  15995  prodss  16000  fprod2dlem  16033  fproddivf  16040  fprodsplitf  16041  rpnnen2lem10  16278  cpnnen  16284  sumeven  16444  sumodd  16445  sadcp1  16512  smupp1  16537  pcmptdvds  16953  prmreclem2  16976  prmreclem5  16979  prmreclem6  16980  prmrec  16981  prmdvdsprmo  17101  iscatd2  17736  initoeu2  18072  yoniso  18340  sgrpidmnd  18796  mndind  18886  eqg0subg  19266  symggen  19539  dprd2d2  20115  srhmsubc  20764  isdrngrd  20847  isdrngrdOLD  20849  lbspss  21180  frlmphl  21899  frlmup1  21916  opsrtoslem1  22174  selvvvval  22261  mdetralt  22733  mdetralt2  22734  mdetunilem2  22738  maducoeval2  22765  chfacfscmulgsum  22985  chfacfpmmulgsum  22989  isclo2  23213  neiptopnei  23257  ptcldmpt  23739  elmptrab  23952  hausflimi  24105  hausflim  24106  alexsubALTlem3  24174  alexsubALTlem4  24175  ptcmplem2  24178  cnextcn  24192  cnextfres1  24193  tgphaus  24242  ustuqtop  24371  utopsnneip  24373  ucncn  24409  nrmmetd  24699  xrhmeo  25073  iscau2  25404  caucfil  25410  cmetcaulem  25415  bcth  25456  vitalilem3  25737  vitali  25740  i1f1lem  25816  itg11  25818  i1fres  25832  mbfi1fseq  25848  mbfi1flim  25850  itg2uba  25870  itg2splitlem  25875  isibl2  25893  cbvitg  25903  cbvitgv  25904  itgss3  25942  dvmptfsum  26102  rolle  26117  elply2  26321  plyexmo  26442  lgamgulmlem2  27159  prmorcht  27307  pclogsum  27344  dchr1  27386  lgsdir  27461  lgsdilem2  27462  lgsdi  27463  lgsne0  27464  lgsquadlem3  27511  lgsquad  27512  2sqlem8  27555  nosupcbv  27831  nosupno  27832  nosupdm  27833  nosupbnd1lem1  27837  noinfcbv  27846  noinfno  27847  noinfdm  27848  nocvxminlem  27912  legval  28818  legov  28819  tglineintmo  28876  tglowdim2ln  28886  ishpg  28999  lnopp2hpgb  29003  hpgerlem  29005  colopp  29009  elplngid  29021  lnincplng  29023  plngcp  29025  plngrot  29029  nhpmirhp  29037  lnperpexs  29070  ragraghl  29103  prlnghpg  29150  prlngmo  29156  axcontlem1  29254  numedglnl  29434  uvtxnbgrvtx  29683  cusgrres  29738  wspniunwspnon  30212  rusgrnumwwlkb0  30263  frgr3vlem2  30565  3vfriswmgrlem  30568  fusgr2wsp2nb  30625  numclwlk2lem2f1o  30670  lpni  30772  pjhthmo  31594  chscllem2  31930  cbvdisjf  32856  2ndresdju  32934  fmptcof2  32942  aciunf1lem  32947  funcnv4mpt  32953  suppovss  32966  fpwrelmapffslem  33017  fsumiunle  33113  gsumwrd2dccatlem  33337  elrspunsn  33680  1arithufdlem3  33780  fedgmullem1  33963  fldextrspunlsp  34008  extdgfialglem2  34027  zarclssn  34207  esumcvg  34420  fiunelros  34508  measiun  34552  bnj1146  35123  bnj1185  35125  bnj1385  35164  bnj1014  35293  bnj1112  35315  bnj1123  35318  bnj1228  35343  bnj1326  35358  bnj1321  35359  bnj1384  35364  bnj1417  35373  bnj1497  35392  trssfir1om  35446  r1omhfb  35447  fineqvnttrclse  35459  axregscl  35463  setindregs  35465  trssfir1omregs  35471  r1omhfbregs  35472  onvf1odlem2  35486  onvf1odlem3  35487  gonarlem  35784  goalrlem  35786  goalr  35787  mrsubrn  35903  dfon2lem6  36176  dfbigcup2  36287  lineintmo  36547  cbvralvw2  36626  cbvrexvw2  36627  cbvrmovw2  36628  cbvreuvw2  36629  cbvmptvw2  36634  cbvprodvw2  36647  cbvrmodavw  36652  cbvreudavw  36653  cbvrabdavw  36661  cbvmptdavw  36667  cbvriotadavw  36670  cbvixpdavw  36678  cbvproddavw  36680  cbvitgdavw  36681  cbvrabdavw2  36685  cbvmptdavw2  36688  cbvriotadavw2  36690  weiunlem  36862  dfttc4  36929  mh-infprim2bi  36946  eleq2w2ALT  37570  bj-idres  37691  mptsnunlem  37871  wl-dfcleq  38047  wl-dfclel  38048  ptrest  38157  poimirlem25  38183  mblfinlem2  38196  mblfinlem3  38197  mblfinlem4  38198  ismblfin  38199  mbfposadd  38205  itg2addnclem  38209  ftc1anclem5  38235  ftc1anclem6  38236  ftc1anclem7  38237  ftc1anc  38239  areacirclem5  38250  fdc1  38284  inxprnres  38836  fsumshftd  39615  pmapglb  40433  polval2N  40569  osumcllem4N  40622  pexmidlem1N  40633  dih1dimatlem  41992  mapdh9a  42452  mapdh9aOLDN  42453  sticksstones2  42803  fsuppind  43213  fphpd  43434  fphpdo  43435  pellex  43453  setindtrs  43643  dford3lem2  43645  fnwe2lem2  43669  mendlmod  43807  cantnfub  43939  tfsconcat0i  43963  rababg  44191  fsovrfovd  44626  fsovcnvlem  44630  trfr  45562  elunif  45627  iunincfi  45703  cbvmpo2  45706  cbvmpo1  45707  disjf1  45792  wessf1ornlem  45794  disjinfi  45801  supxrleubrnmptf  46056  monoordxr  46087  monoord2xr  46089  fsummulc1f  46178  fsumnncl  46179  fsumf1of  46181  fsumiunss  46182  fsumreclf  46183  fsumlessf  46184  fsumsermpt  46186  fmulcl  46188  fmul01lt1lem2  46192  fprodexp  46201  fprodabs2  46202  climmulf  46211  climexp  46212  climrecf  46216  climinff  46218  climaddf  46222  mullimc  46223  limcperiod  46235  sumnnodd  46237  neglimc  46252  addlimc  46253  climsubmpt  46265  climreclf  46269  climeldmeqmpt  46273  climfveqmpt  46276  fnlimfvre  46279  climfveqf  46285  climfveqmpt3  46287  climeldmeqf  46288  climeqf  46293  climeldmeqmpt3  46294  climinf2  46312  limsupequz  46328  limsupequzmptf  46336  lmbr3  46352  cnrefiisp  46435  cncfshift  46479  fprodcncf  46505  dvmptmulf  46542  dvmptfprod  46550  dvnprodlem1  46551  dvnprodlem3  46553  stoweidlem16  46621  stoweidlem34  46639  stoweidlem62  46667  dirkercncflem2  46709  fourierdlem12  46724  fourierdlem15  46727  fourierdlem34  46746  fourierdlem50  46761  fourierdlem73  46784  fourierdlem94  46805  fourierdlem112  46823  fourierdlem113  46824  intsaluni  46934  sge0lempt  47015  sge0iunmptlemfi  47018  sge0iunmptlemre  47020  sge0iunmpt  47023  sge0ltfirpmpt2  47031  sge0isummpt2  47037  sge0xaddlem2  47039  sge0xadd  47040  meadjiun  47071  voliunsge0lem  47077  meaiuninclem  47085  meaiunincf  47088  meaiuninc3v  47089  meaiuninc3  47090  meaiininclem  47091  meaiininc  47092  isomennd  47136  ovn0lem  47170  sge0hsphoire  47194  hoidmvlelem1  47200  hoidmvlelem2  47201  hoidmvlelem3  47202  hoidmvlelem5  47204  hspmbllem2  47232  hoimbl2  47270  vonhoire  47277  vonioo  47287  vonicc  47290  vonn0ioo2  47295  vonn0icc2  47297  pimincfltioc  47321  salpreimagtlt  47335  smflimlem4  47379  ormkglobd  47482  sinnpoly  47516  rexrsb  47725  ichexmpl2  48107  ichnreuop  48109  sbgoldbm  48437  bgoldbnnsum3prm  48457  tgoldbach  48470  srhmsubcALTV  48978  cbvmpox2  49000  mo0sn  49478  f1omoOLD  49556  isthincd2lem1  50087  thincmo  50090  euendfunc  50188