Theorem eleq1w 2821

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

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813

This theorem is referenced by:  clelsb1  2865  cleqh  2868  nfcjust  2888  nfcr  2892  cleqf  2931  rspw  3233  cbvralvw  3234  cbvrexvw  3235  cbvralfw  3301  cbvralsvw  3314  cbvralf  3357  ralcom2  3374  moel  3399  cbvrmovw  3400  cbvreuvw  3401  moelOLD  3402  cbvrmow  3406  cbvreuwOLD  3412  cbvreu  3424  cbvrabv  3443  rabrabi  3452  cbvrabw  3470  cbvrabwOLD  3471  nfrab  3475  cbvrab  3476  elrab2w  3698  reu2  3733  reu6  3734  rmo4  3738  reu8  3741  2reu5  3766  ruOLD  3789  csbied  3945  difjust  3964  unjust  3966  injust  3968  dfss2  3980  dfssf  3985  dfdif3OLD  4127  eqeuel  4370  rabeq0w  4392  disj  4455  reldisj  4458  ralidmw  4513  dfif6  4533  rabsnifsb  4726  eluniab  4925  unissb  4943  elintabOLD  4963  uniintsn  4989  dfiun2g  5034  dfiunv2  5039  disjxun  5145  cbvmptf  5256  cbvmptfg  5257  cbvmptv  5260  dftr2c  5267  isso2i  5632  dfres2  6060  imai  6093  frpoinsg  6365  wfisgOLD  6376  tz7.7  6411  fvn0ssdmfun  7093  fmptco  7148  cbvriotaw  7396  cbvriotavw  7397  cbvriota  7400  cbvmpox  7525  cbvmpov  7527  tfis  7875  tfindes  7883  peano5  7915  findes  7922  dfoprab4f  8079  fmpox  8090  xpord2indlem  8170  poseq  8181  soseq  8182  wfrlem10OLD  8356  smogt  8405  resixpfo  8974  ixpsnf1o  8976  dom2lem  9030  mapsnend  9074  pw2f1olem  9114  pssnn  9206  ssfi  9211  findcard3  9315  findcard3OLD  9316  ordiso2  9552  elirrv  9633  cantnflem1d  9725  cantnf  9730  setind  9771  frinsg  9788  tz9.12lem3  9826  infxpen  10051  dfac5lem4  10163  dfac12lem2  10182  kmlem14  10201  cfsmolem  10307  sornom  10314  isf32lem9  10398  axdc2  10486  fpwwe2lem7  10674  fpwwe2  10680  wunex2  10775  dedekindle  11422  wloglei  11792  uzind4s  12947  seqof2  14097  reuccatpfxs1  14781  shftfn  15108  rexuz3  15383  zsum  15750  fsum  15752  sumss  15756  sumss2  15758  fsumcvg2  15759  fsumser  15762  fsumclf  15770  fsumsplitf  15774  isumless  15877  prodfdiv  15928  cbvprod  15945  cbvprodv  15946  zprod  15969  fprod  15973  fprodntriv  15974  prodss  15979  fprod2dlem  16012  fproddivf  16019  fprodsplitf  16020  rpnnen2lem10  16255  cpnnen  16261  sumeven  16420  sumodd  16421  sadcp1  16488  smupp1  16513  pcmptdvds  16927  prmreclem2  16950  prmreclem5  16953  prmreclem6  16954  prmrec  16955  prmdvdsprmo  17075  iscatd2  17725  initoeu2  18069  yoniso  18341  sgrpidmnd  18764  mndind  18853  eqg0subg  19226  symggen  19502  dprd2d2  20078  srhmsubc  20696  isdrngrd  20782  isdrngrdOLD  20784  lbspss  21098  frlmphl  21818  frlmup1  21835  opsrtoslem1  22096  mdetralt  22629  mdetralt2  22630  mdetunilem2  22634  maducoeval2  22661  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  isclo2  23111  neiptopnei  23155  ptcldmpt  23637  elmptrab  23850  hausflimi  24003  hausflim  24004  alexsubALTlem3  24072  alexsubALTlem4  24073  ptcmplem2  24076  cnextcn  24090  cnextfres1  24091  tgphaus  24140  ustuqtop  24270  utopsnneip  24272  ucncn  24309  nrmmetd  24602  xrhmeo  24990  iscau2  25324  caucfil  25330  cmetcaulem  25335  bcth  25376  vitalilem3  25658  vitali  25661  i1f1lem  25737  itg11  25739  i1fres  25754  mbfi1fseq  25770  mbfi1flim  25772  itg2uba  25792  itg2splitlem  25797  isibl2  25815  cbvitg  25825  cbvitgv  25826  itgss3  25864  dvmptfsum  26027  rolle  26042  elply2  26249  plyexmo  26369  lgamgulmlem2  27087  prmorcht  27235  pclogsum  27273  dchr1  27315  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  lgsquadlem3  27440  lgsquad  27441  2sqlem8  27484  nosupcbv  27761  nosupno  27762  nosupdm  27763  nosupbnd1lem1  27767  noinfcbv  27776  noinfno  27777  noinfdm  27778  nocvxminlem  27836  legval  28606  legov  28607  tglineintmo  28664  tglowdim2ln  28673  ishpg  28781  lnopp2hpgb  28785  hpgerlem  28787  colopp  28791  axcontlem1  28993  numedglnl  29175  uvtxnbgrvtx  29424  cusgrres  29480  wspniunwspnon  29952  rusgrnumwwlkb0  30000  frgr3vlem2  30302  3vfriswmgrlem  30305  fusgr2wsp2nb  30362  numclwlk2lem2f1o  30407  lpni  30508  pjhthmo  31330  chscllem2  31666  cbvdisjf  32590  2ndresdju  32665  fmptcof2  32673  aciunf1lem  32678  funcnv4mpt  32685  suppovss  32695  fpwrelmapffslem  32749  fsumiunle  32835  gsumwrd2dccatlem  33051  elrspunsn  33436  1arithufdlem3  33553  fedgmullem1  33656  zarclssn  33833  esumcvg  34066  fiunelros  34154  measiun  34198  bnj1146  34783  bnj1185  34785  bnj1385  34824  bnj1014  34953  bnj1112  34975  bnj1123  34978  bnj1228  35003  bnj1326  35018  bnj1321  35019  bnj1384  35024  bnj1417  35033  bnj1497  35052  gonarlem  35378  goalrlem  35380  goalr  35381  mrsubrn  35497  dfon2lem6  35769  dfbigcup2  35880  lineintmo  36138  cbvralvw2  36208  cbvrexvw2  36209  cbvrmovw2  36210  cbvreuvw2  36211  cbvmptvw2  36216  cbvprodvw2  36229  cbvrmodavw  36234  cbvreudavw  36235  cbvrabdavw  36243  cbvmptdavw  36249  cbvriotadavw  36252  cbvixpdavw  36260  cbvproddavw  36262  cbvitgdavw  36263  cbvrabdavw2  36267  cbvmptdavw2  36270  cbvriotadavw2  36272  weiunlem2  36445  eleq2w2ALT  37029  bj-idres  37142  mptsnunlem  37320  ptrest  37605  poimirlem25  37631  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  mbfposadd  37653  itg2addnclem  37657  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anc  37687  areacirclem5  37698  fdc1  37732  inxprnres  38273  fsumshftd  38933  pmapglb  39752  polval2N  39888  osumcllem4N  39941  pexmidlem1N  39952  dih1dimatlem  41311  mapdh9a  41771  mapdh9aOLDN  41772  sticksstones2  42128  selvvvval  42571  fsuppind  42576  fphpd  42803  fphpdo  42804  pellex  42822  setindtrs  43013  dford3lem2  43015  fnwe2lem2  43039  mendlmod  43177  cantnfub  43310  tfsconcat0i  43334  rababg  43563  fsovrfovd  43998  fsovcnvlem  44002  scottabf  44235  elunif  44953  iunincfi  45033  cbvmpo2  45036  cbvmpo1  45037  disjf1  45125  wessf1ornlem  45127  disjinfi  45134  supxrleubrnmptf  45400  monoordxr  45432  monoord2xr  45434  fsummulc1f  45526  fsumnncl  45527  fsumf1of  45529  fsumiunss  45530  fsumreclf  45531  fsumlessf  45532  fsumsermpt  45534  fmulcl  45536  fmul01lt1lem2  45540  fprodexp  45549  fprodabs2  45550  climmulf  45559  climexp  45560  climrecf  45564  climinff  45566  climaddf  45570  mullimc  45571  limcperiod  45583  sumnnodd  45585  neglimc  45602  addlimc  45603  climsubmpt  45615  climreclf  45619  climeldmeqmpt  45623  climfveqmpt  45626  fnlimfvre  45629  climfveqf  45635  climfveqmpt3  45637  climeldmeqf  45638  climeqf  45643  climeldmeqmpt3  45644  climinf2  45662  limsupequz  45678  limsupequzmptf  45686  lmbr3  45702  cnrefiisp  45785  cncfshift  45829  fprodcncf  45855  dvmptmulf  45892  dvmptfprod  45900  dvnprodlem1  45901  dvnprodlem3  45903  stoweidlem16  45971  stoweidlem34  45989  stoweidlem62  46017  dirkercncflem2  46059  fourierdlem12  46074  fourierdlem15  46077  fourierdlem34  46096  fourierdlem50  46111  fourierdlem73  46134  fourierdlem94  46155  fourierdlem112  46173  fourierdlem113  46174  intsaluni  46284  sge0lempt  46365  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0ltfirpmpt2  46381  sge0isummpt2  46387  sge0xaddlem2  46389  sge0xadd  46390  meadjiun  46421  voliunsge0lem  46427  meaiuninclem  46435  meaiunincf  46438  meaiuninc3v  46439  meaiuninc3  46440  meaiininclem  46441  meaiininc  46442  isomennd  46486  ovn0lem  46520  sge0hsphoire  46544  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem5  46554  hspmbllem2  46582  hoimbl2  46620  vonhoire  46627  vonioo  46637  vonicc  46640  vonn0ioo2  46645  vonn0icc2  46647  pimincfltioc  46671  salpreimagtlt  46685  smflimlem4  46729  rexrsb  47049  ichexmpl2  47394  ichnreuop  47396  sbgoldbm  47708  bgoldbnnsum3prm  47728  tgoldbach  47741  srhmsubcALTV  48168  cbvmpox2  48180  mo0sn  48663  f1omo  48690  isthincd2lem1  48826  thincmo  48828