Theorem eleq1w 2822

Description: Weaker version of eleq1 2827 (but more general than elequ1 2126) not depending on ax-ext 2711 nor df-cleq 2731.

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814

This theorem is referenced by:  clelsb1  2866  cleqh  2868  nfcjust  2887  nfcr  2891  cleqf  2929  rspw  3216  cbvralvw  3217  cbvrexvw  3218  cbvralfw  3279  cbvralsvw  3290  cbvralf  3324  ralcom2  3341  moel  3364  cbvrmovw  3365  cbvreuvw  3366  cbvrmow  3369  cbvreu  3383  cbvrabv  3401  rabrabi  3410  cbvrabw  3426  cbvrabwOLD  3427  nfrab  3429  cbvrab  3430  elrab2w  3633  reu2  3666  reu6  3667  rmo4  3671  reu8  3674  2reu5  3699  ruOLD  3722  csbied  3867  difjust  3885  unjust  3887  injust  3889  dfss2  3901  dfssf  3906  dfdif3OLD  4049  eqeuel  4293  rabeq0w  4315  disj  4378  reldisj  4381  ralidmw  4444  dfif6  4457  rabsnifsb  4654  eluniab  4852  unissb  4871  uniintsn  4915  dfiun2g  4959  dfiunv2  4963  disjxun  5070  cbvmptf  5172  cbvmptfg  5173  cbvmptv  5176  dftr2c  5182  isso2i  5563  dfres2  5993  imai  6026  frpoinsg  6294  tz7.7  6336  fvn0ssdmfun  7015  fmptco  7071  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  8874  ixpsnf1o  8876  dom2lem  8929  mapsnend  8973  pw2f1olem  9009  pssnn  9093  ssfi  9097  findcard3  9183  ordiso2  9420  elirrvOLDOLD  9504  cantnflem1d  9600  cantnf  9605  setind  9659  frinsg  9666  tz9.12lem3  9704  infxpen  9927  dfac5lem4  10039  dfac12lem2  10058  kmlem14  10077  cfsmolem  10183  sornom  10190  isf32lem9  10274  axdc2  10362  fpwwe2lem7  10551  fpwwe2  10557  wunex2  10652  dedekindle  11301  wloglei  11673  uzind4s  12849  seqof2  14013  reuccatpfxs1  14700  shftfn  15026  rexuz3  15302  zsum  15671  fsum  15673  sumss  15677  sumss2  15679  fsumcvg2  15680  fsumser  15683  fsumclf  15691  fsumsplitf  15695  isumless  15801  prodfdiv  15852  cbvprod  15869  cbvprodv  15870  zprod  15893  fprod  15897  fprodntriv  15898  prodss  15903  fprod2dlem  15936  fproddivf  15943  fprodsplitf  15944  rpnnen2lem10  16181  cpnnen  16187  sumeven  16347  sumodd  16348  sadcp1  16415  smupp1  16440  pcmptdvds  16856  prmreclem2  16879  prmreclem5  16882  prmreclem6  16883  prmrec  16884  prmdvdsprmo  17004  iscatd2  17638  initoeu2  17974  yoniso  18242  sgrpidmnd  18698  mndind  18787  eqg0subg  19162  symggen  19436  dprd2d2  20012  srhmsubc  20652  isdrngrd  20738  isdrngrdOLD  20740  lbspss  21072  frlmphl  21756  frlmup1  21773  opsrtoslem1  22031  selvvvval  22118  mdetralt  22591  mdetralt2  22592  mdetunilem2  22596  maducoeval2  22623  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  isclo2  23071  neiptopnei  23115  ptcldmpt  23597  elmptrab  23810  hausflimi  23963  hausflim  23964  alexsubALTlem3  24032  alexsubALTlem4  24033  ptcmplem2  24036  cnextcn  24050  cnextfres1  24051  tgphaus  24100  ustuqtop  24229  utopsnneip  24231  ucncn  24267  nrmmetd  24557  xrhmeo  24931  iscau2  25262  caucfil  25268  cmetcaulem  25273  bcth  25314  vitalilem3  25595  vitali  25598  i1f1lem  25674  itg11  25676  i1fres  25690  mbfi1fseq  25706  mbfi1flim  25708  itg2uba  25728  itg2splitlem  25733  isibl2  25751  cbvitg  25761  cbvitgv  25762  itgss3  25800  dvmptfsum  25960  rolle  25975  elply2  26179  plyexmo  26297  lgamgulmlem2  27011  prmorcht  27159  pclogsum  27196  dchr1  27238  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  lgsne0  27316  lgsquadlem3  27363  lgsquad  27364  2sqlem8  27407  nosupcbv  27684  nosupno  27685  nosupdm  27686  nosupbnd1lem1  27690  noinfcbv  27699  noinfno  27700  noinfdm  27701  nocvxminlem  27764  legval  28670  legov  28671  tglineintmo  28728  tglowdim2ln  28737  ishpg  28845  lnopp2hpgb  28849  hpgerlem  28851  colopp  28855  axcontlem1  29051  numedglnl  29231  uvtxnbgrvtx  29480  cusgrres  29535  wspniunwspnon  30009  rusgrnumwwlkb0  30060  frgr3vlem2  30362  3vfriswmgrlem  30365  fusgr2wsp2nb  30422  numclwlk2lem2f1o  30467  lpni  30569  pjhthmo  31391  chscllem2  31727  cbvdisjf  32660  2ndresdju  32741  fmptcof2  32749  aciunf1lem  32754  funcnv4mpt  32760  suppovss  32773  fpwrelmapffslem  32824  fsumiunle  32921  gsumwrd2dccatlem  33158  elrspunsn  33512  1arithufdlem3  33629  fedgmullem1  33813  fldextrspunlsp  33858  extdgfialglem2  33877  zarclssn  34057  esumcvg  34270  fiunelros  34358  measiun  34402  bnj1146  34973  bnj1185  34975  bnj1385  35014  bnj1014  35143  bnj1112  35165  bnj1123  35168  bnj1228  35193  bnj1326  35208  bnj1321  35209  bnj1384  35214  bnj1417  35223  bnj1497  35242  trssfir1om  35292  r1omhfb  35293  fineqvnttrclse  35305  axregscl  35309  setindregs  35311  trssfir1omregs  35317  r1omhfbregs  35318  onvf1odlem2  35332  onvf1odlem3  35333  gonarlem  35622  goalrlem  35624  goalr  35625  mrsubrn  35741  dfon2lem6  36014  dfbigcup2  36125  lineintmo  36385  cbvralvw2  36454  cbvrexvw2  36455  cbvrmovw2  36456  cbvreuvw2  36457  cbvmptvw2  36462  cbvprodvw2  36475  cbvrmodavw  36480  cbvreudavw  36481  cbvrabdavw  36489  cbvmptdavw  36495  cbvriotadavw  36498  cbvixpdavw  36506  cbvproddavw  36508  cbvitgdavw  36509  cbvrabdavw2  36513  cbvmptdavw2  36516  cbvriotadavw2  36518  weiunlem  36691  dfttc4  36758  mh-infprim2bi  36775  eleq2w2ALT  37400  bj-idres  37520  mptsnunlem  37700  wl-dfcleq  37876  wl-dfclel  37877  ptrest  37986  poimirlem25  38012  mblfinlem2  38025  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  mbfposadd  38034  itg2addnclem  38038  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anc  38068  areacirclem5  38079  fdc1  38113  inxprnres  38665  fsumshftd  39444  pmapglb  40262  polval2N  40398  osumcllem4N  40451  pexmidlem1N  40462  dih1dimatlem  41821  mapdh9a  42281  mapdh9aOLDN  42282  sticksstones2  42632  fsuppind  43040  fphpd  43261  fphpdo  43262  pellex  43280  setindtrs  43470  dford3lem2  43472  fnwe2lem2  43496  mendlmod  43634  cantnfub  43766  tfsconcat0i  43790  rababg  44018  fsovrfovd  44453  fsovcnvlem  44457  scottabf  44684  trfr  45406  elunif  45464  iunincfi  45541  cbvmpo2  45544  cbvmpo1  45545  disjf1  45630  wessf1ornlem  45632  disjinfi  45639  supxrleubrnmptf  45894  monoordxr  45925  monoord2xr  45927  fsummulc1f  46016  fsumnncl  46017  fsumf1of  46019  fsumiunss  46020  fsumreclf  46021  fsumlessf  46022  fsumsermpt  46024  fmulcl  46026  fmul01lt1lem2  46030  fprodexp  46039  fprodabs2  46040  climmulf  46049  climexp  46050  climrecf  46054  climinff  46056  climaddf  46060  mullimc  46061  limcperiod  46073  sumnnodd  46075  neglimc  46090  addlimc  46091  climsubmpt  46103  climreclf  46107  climeldmeqmpt  46111  climfveqmpt  46114  fnlimfvre  46117  climfveqf  46123  climfveqmpt3  46125  climeldmeqf  46126  climeqf  46131  climeldmeqmpt3  46132  climinf2  46150  limsupequz  46166  limsupequzmptf  46174  lmbr3  46190  cnrefiisp  46273  cncfshift  46317  fprodcncf  46343  dvmptmulf  46380  dvmptfprod  46388  dvnprodlem1  46389  dvnprodlem3  46391  stoweidlem16  46459  stoweidlem34  46477  stoweidlem62  46505  dirkercncflem2  46547  fourierdlem12  46562  fourierdlem15  46565  fourierdlem34  46584  fourierdlem50  46599  fourierdlem73  46622  fourierdlem94  46643  fourierdlem112  46661  fourierdlem113  46662  intsaluni  46772  sge0lempt  46853  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0iunmpt  46861  sge0ltfirpmpt2  46869  sge0isummpt2  46875  sge0xaddlem2  46877  sge0xadd  46878  meadjiun  46909  voliunsge0lem  46915  meaiuninclem  46923  meaiunincf  46926  meaiuninc3v  46927  meaiuninc3  46928  meaiininclem  46929  meaiininc  46930  isomennd  46974  ovn0lem  47008  sge0hsphoire  47032  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem5  47042  hspmbllem2  47070  hoimbl2  47108  vonhoire  47115  vonioo  47125  vonicc  47128  vonn0ioo2  47133  vonn0icc2  47135  pimincfltioc  47159  salpreimagtlt  47173  smflimlem4  47217  ormkglobd  47320  sinnpoly  47354  rexrsb  47563  ichexmpl2  47945  ichnreuop  47947  sbgoldbm  48275  bgoldbnnsum3prm  48295  tgoldbach  48308  srhmsubcALTV  48816  cbvmpox2  48827  mo0sn  49306  f1omoOLD  49384  isthincd2lem1  49915  thincmo  49918  euendfunc  50016