Theorem eleq1w 2827

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

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819

This theorem is referenced by:  clelsb1  2871  cleqh  2874  nfcjust  2894  nfcr  2898  cleqf  2940  rspw  3242  cbvralvw  3243  cbvrexvw  3244  cbvralfw  3310  cbvralsvw  3323  cbvralf  3368  ralcom2  3385  moel  3410  cbvrmovw  3411  cbvreuvw  3412  moelOLD  3413  cbvrmow  3417  cbvreuwOLD  3423  cbvreu  3435  cbvrabv  3454  rabrabi  3463  cbvrabw  3481  cbvrabwOLD  3482  nfrab  3486  cbvrab  3487  elrab2w  3712  reu2  3747  reu6  3748  rmo4  3752  reu8  3755  2reu5  3780  ruOLD  3803  csbied  3959  difjust  3978  unjust  3980  injust  3982  dfss2  3994  dfssf  3999  dfdif3OLD  4141  eqeuel  4388  rabeq0w  4410  disj  4473  reldisj  4476  ralidmw  4531  dfif6  4551  rabsnifsb  4747  eluniab  4945  unissb  4963  elintabOLD  4983  uniintsn  5009  dfiun2g  5053  dfiunv2  5058  disjxun  5164  cbvmptf  5275  cbvmptfg  5276  cbvmptv  5279  dftr2c  5286  isso2i  5644  dfres2  6070  imai  6103  frpoinsg  6375  wfisgOLD  6386  tz7.7  6421  fvn0ssdmfun  7108  fmptco  7163  cbvriotaw  7413  cbvriotavw  7414  cbvriota  7418  cbvmpox  7543  cbvmpov  7545  tfis  7892  tfindes  7900  peano5  7932  findes  7940  dfoprab4f  8097  fmpox  8108  xpord2indlem  8188  poseq  8199  soseq  8200  wfrlem10OLD  8374  smogt  8423  resixpfo  8994  ixpsnf1o  8996  dom2lem  9052  mapsnend  9101  pw2f1olem  9142  pssnn  9234  ssfi  9240  findcard3  9346  findcard3OLD  9347  ordiso2  9584  elirrv  9665  cantnflem1d  9757  cantnf  9762  setind  9803  frinsg  9820  tz9.12lem3  9858  infxpen  10083  dfac5lem4  10195  dfac12lem2  10214  kmlem14  10233  cfsmolem  10339  sornom  10346  isf32lem9  10430  axdc2  10518  fpwwe2lem7  10706  fpwwe2  10712  wunex2  10807  dedekindle  11454  wloglei  11822  uzind4s  12973  seqof2  14111  reuccatpfxs1  14795  shftfn  15122  rexuz3  15397  zsum  15766  fsum  15768  sumss  15772  sumss2  15774  fsumcvg2  15775  fsumser  15778  fsumclf  15786  fsumsplitf  15790  isumless  15893  prodfdiv  15944  cbvprod  15961  cbvprodv  15962  zprod  15985  fprod  15989  fprodntriv  15990  prodss  15995  fprod2dlem  16028  fproddivf  16035  fprodsplitf  16036  rpnnen2lem10  16271  cpnnen  16277  sumeven  16435  sumodd  16436  sadcp1  16501  smupp1  16526  pcmptdvds  16941  prmreclem2  16964  prmreclem5  16967  prmreclem6  16968  prmrec  16969  prmdvdsprmo  17089  iscatd2  17739  initoeu2  18083  yoniso  18355  sgrpidmnd  18777  mndind  18863  eqg0subg  19236  symggen  19512  dprd2d2  20088  srhmsubc  20702  isdrngrd  20788  isdrngrdOLD  20790  lbspss  21104  frlmphl  21824  frlmup1  21841  opsrtoslem1  22102  mdetralt  22635  mdetralt2  22636  mdetunilem2  22640  maducoeval2  22667  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  isclo2  23117  neiptopnei  23161  ptcldmpt  23643  elmptrab  23856  hausflimi  24009  hausflim  24010  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem2  24082  cnextcn  24096  cnextfres1  24097  tgphaus  24146  ustuqtop  24276  utopsnneip  24278  ucncn  24315  nrmmetd  24608  xrhmeo  24996  iscau2  25330  caucfil  25336  cmetcaulem  25341  bcth  25382  vitalilem3  25664  vitali  25667  i1f1lem  25743  itg11  25745  i1fres  25760  mbfi1fseq  25776  mbfi1flim  25778  itg2uba  25798  itg2splitlem  25803  isibl2  25821  cbvitg  25831  cbvitgv  25832  itgss3  25870  dvmptfsum  26033  rolle  26048  elply2  26255  plyexmo  26373  lgamgulmlem2  27091  prmorcht  27239  pclogsum  27277  dchr1  27319  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  lgsquadlem3  27444  lgsquad  27445  2sqlem8  27488  nosupcbv  27765  nosupno  27766  nosupdm  27767  nosupbnd1lem1  27771  noinfcbv  27780  noinfno  27781  noinfdm  27782  nocvxminlem  27840  legval  28610  legov  28611  tglineintmo  28668  tglowdim2ln  28677  ishpg  28785  lnopp2hpgb  28789  hpgerlem  28791  colopp  28795  axcontlem1  28997  numedglnl  29179  uvtxnbgrvtx  29428  cusgrres  29484  wspniunwspnon  29956  rusgrnumwwlkb0  30004  frgr3vlem2  30306  3vfriswmgrlem  30309  fusgr2wsp2nb  30366  numclwlk2lem2f1o  30411  lpni  30512  pjhthmo  31334  chscllem2  31670  cbvdisjf  32593  2ndresdju  32667  fmptcof2  32675  aciunf1lem  32680  funcnv4mpt  32687  suppovss  32697  fpwrelmapffslem  32746  fsumiunle  32833  elrspunsn  33422  1arithufdlem3  33539  fedgmullem1  33642  zarclssn  33819  esumcvg  34050  fiunelros  34138  measiun  34182  bnj1146  34767  bnj1185  34769  bnj1385  34808  bnj1014  34937  bnj1112  34959  bnj1123  34962  bnj1228  34987  bnj1326  35002  bnj1321  35003  bnj1384  35008  bnj1417  35017  bnj1497  35036  gonarlem  35362  goalrlem  35364  goalr  35365  mrsubrn  35481  dfon2lem6  35752  dfbigcup2  35863  lineintmo  36121  cbvralvw2  36192  cbvrexvw2  36193  cbvrmovw2  36194  cbvreuvw2  36195  cbvmptvw2  36200  cbvprodvw2  36213  cbvrmodavw  36218  cbvreudavw  36219  cbvrabdavw  36227  cbvmptdavw  36233  cbvriotadavw  36236  cbvixpdavw  36244  cbvproddavw  36246  cbvitgdavw  36247  cbvrabdavw2  36251  cbvmptdavw2  36254  cbvriotadavw2  36256  weiunlem2  36429  eleq2w2ALT  37013  bj-idres  37126  mptsnunlem  37304  ptrest  37579  poimirlem25  37605  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  mbfposadd  37627  itg2addnclem  37631  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anc  37661  areacirclem5  37672  fdc1  37706  inxprnres  38248  fsumshftd  38908  pmapglb  39727  polval2N  39863  osumcllem4N  39916  pexmidlem1N  39927  dih1dimatlem  41286  mapdh9a  41746  mapdh9aOLDN  41747  sticksstones2  42104  selvvvval  42540  fsuppind  42545  fphpd  42772  fphpdo  42773  pellex  42791  setindtrs  42982  dford3lem2  42984  fnwe2lem2  43008  mendlmod  43150  cantnfub  43283  tfsconcat0i  43307  rababg  43536  fsovrfovd  43971  fsovcnvlem  43975  scottabf  44209  elunif  44916  iunincfi  44996  cbvmpo2  44999  cbvmpo1  45000  disjf1  45090  wessf1ornlem  45092  disjinfi  45099  supxrleubrnmptf  45366  monoordxr  45398  monoord2xr  45400  fsummulc1f  45492  fsumnncl  45493  fsumf1of  45495  fsumiunss  45496  fsumreclf  45497  fsumlessf  45498  fsumsermpt  45500  fmulcl  45502  fmul01lt1lem2  45506  fprodexp  45515  fprodabs2  45516  climmulf  45525  climexp  45526  climrecf  45530  climinff  45532  climaddf  45536  mullimc  45537  limcperiod  45549  sumnnodd  45551  neglimc  45568  addlimc  45569  climsubmpt  45581  climreclf  45585  climeldmeqmpt  45589  climfveqmpt  45592  fnlimfvre  45595  climfveqf  45601  climfveqmpt3  45603  climeldmeqf  45604  climeqf  45609  climeldmeqmpt3  45610  climinf2  45628  limsupequz  45644  limsupequzmptf  45652  lmbr3  45668  cnrefiisp  45751  cncfshift  45795  fprodcncf  45821  dvmptmulf  45858  dvmptfprod  45866  dvnprodlem1  45867  dvnprodlem3  45869  stoweidlem16  45937  stoweidlem34  45955  stoweidlem62  45983  dirkercncflem2  46025  fourierdlem12  46040  fourierdlem15  46043  fourierdlem34  46062  fourierdlem50  46077  fourierdlem73  46100  fourierdlem94  46121  fourierdlem112  46139  fourierdlem113  46140  intsaluni  46250  sge0lempt  46331  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0ltfirpmpt2  46347  sge0isummpt2  46353  sge0xaddlem2  46355  sge0xadd  46356  meadjiun  46387  voliunsge0lem  46393  meaiuninclem  46401  meaiunincf  46404  meaiuninc3v  46405  meaiuninc3  46406  meaiininclem  46407  meaiininc  46408  isomennd  46452  ovn0lem  46486  sge0hsphoire  46510  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem5  46520  hspmbllem2  46548  hoimbl2  46586  vonhoire  46593  vonioo  46603  vonicc  46606  vonn0ioo2  46611  vonn0icc2  46613  pimincfltioc  46637  salpreimagtlt  46651  smflimlem4  46695  rexrsb  47015  ichexmpl2  47344  ichnreuop  47346  sbgoldbm  47658  bgoldbnnsum3prm  47678  tgoldbach  47691  srhmsubcALTV  48048  cbvmpox2  48060  mo0sn  48547  f1omo  48574  isthincd2lem1  48694  thincmo  48696