Theorem eleq1w 2811

Description: Weaker version of eleq1 2816 (but more general than elequ1 2106) not depending on ax-ext 2698 nor df-cleq 2719.

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∃wex 1774   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-clel 2805

This theorem is referenced by:  clelsb1  2855  cleqh  2858  nfcjust  2879  nfcr  2883  nfcriOLD  2888  nfcriOLDOLD  2889  cleqf  2929  rspw  3228  cbvralvw  3229  cbvrexvw  3230  cbvralfw  3296  cbvralfwOLD  3315  cbvralf  3351  ralcom2  3368  moel  3393  cbvrmovw  3394  cbvreuvw  3395  moelOLD  3396  cbvrmow  3400  cbvreuwOLD  3407  cbvreu  3419  cbvrabv  3437  rabrabi  3445  cbvrabw  3462  nfrab  3467  cbvrab  3468  reu2  3718  reu6  3719  rmo4  3723  reu8  3726  2reu5  3751  ru  3773  csbied  3927  difjust  3946  unjust  3948  injust  3950  dfss2f  3968  dfdif3  4110  eqeuel  4358  rabeq0w  4379  disj  4443  reldisj  4447  ralidmw  4503  dfif6  4527  rabsnifsb  4722  eluniab  4917  unissb  4937  elintabOLD  4957  uniintsn  4985  dfiun2g  5027  dfiunv2  5032  disjxun  5140  cbvmptf  5251  cbvmptfg  5252  cbvmptv  5255  dftr2c  5262  isso2i  5619  dfres2  6039  imai  6071  frpoinsg  6343  wfisgOLD  6354  tz7.7  6389  fvn0ssdmfun  7078  fmptco  7132  cbvriotaw  7379  cbvriotavw  7380  cbvriota  7384  cbvmpox  7507  tfis  7853  tfindes  7861  peano5  7893  findes  7902  dfoprab4f  8054  fmpox  8065  xpord2indlem  8146  poseq  8157  soseq  8158  wfrlem10OLD  8332  smogt  8381  resixpfo  8946  ixpsnf1o  8948  dom2lem  9004  mapsnend  9052  pw2f1olem  9092  pssnn  9184  ssfi  9189  findcard3  9301  findcard3OLD  9302  ordiso2  9530  elirrv  9611  cantnflem1d  9703  cantnf  9708  setind  9749  frinsg  9766  tz9.12lem3  9804  infxpen  10029  dfac12lem2  10159  kmlem14  10178  cfsmolem  10285  sornom  10292  isf32lem9  10376  axdc2  10464  fpwwe2lem7  10652  fpwwe2  10658  wunex2  10753  dedekindle  11400  wloglei  11768  uzind4s  12914  seqof2  14049  reuccatpfxs1  14721  shftfn  15044  rexuz3  15319  zsum  15688  fsum  15690  sumss  15694  sumss2  15696  fsumcvg2  15697  fsumser  15700  fsumclf  15708  fsumsplitf  15712  isumless  15815  prodfdiv  15866  cbvprod  15883  zprod  15905  fprod  15909  fprodntriv  15910  prodss  15915  fprod2dlem  15948  fproddivf  15955  fprodsplitf  15956  rpnnen2lem10  16191  cpnnen  16197  sumeven  16355  sumodd  16356  sadcp1  16421  smupp1  16446  pcmptdvds  16854  prmreclem2  16877  prmreclem5  16880  prmreclem6  16881  prmrec  16882  prmdvdsprmo  17002  iscatd2  17652  initoeu2  17996  yoniso  18268  sgrpidmnd  18690  mndind  18771  eqg0subg  19142  symggen  19416  dprd2d2  19992  srhmsubc  20602  isdrngrd  20647  isdrngrdOLD  20649  lbspss  20956  frlmphl  21702  frlmup1  21719  opsrtoslem1  21986  mdetralt  22497  mdetralt2  22498  mdetunilem2  22502  maducoeval2  22529  chfacfscmulgsum  22749  chfacfpmmulgsum  22753  isclo2  22979  neiptopnei  23023  ptcldmpt  23505  elmptrab  23718  hausflimi  23871  hausflim  23872  alexsubALTlem3  23940  alexsubALTlem4  23941  ptcmplem2  23944  cnextcn  23958  cnextfres1  23959  tgphaus  24008  ustuqtop  24138  utopsnneip  24140  ucncn  24177  nrmmetd  24470  xrhmeo  24858  iscau2  25192  caucfil  25198  cmetcaulem  25203  bcth  25244  vitalilem3  25526  vitali  25529  i1f1lem  25605  itg11  25607  i1fres  25622  mbfi1fseq  25638  mbfi1flim  25640  itg2uba  25660  itg2splitlem  25665  isibl2  25683  cbvitg  25692  itgss3  25731  dvmptfsum  25894  rolle  25909  elply2  26117  plyexmo  26235  lgamgulmlem2  26949  prmorcht  27097  pclogsum  27135  dchr1  27177  lgsdir  27252  lgsdilem2  27253  lgsdi  27254  lgsne0  27255  lgsquadlem3  27302  lgsquad  27303  2sqlem8  27346  nosupcbv  27622  nosupno  27623  nosupdm  27624  nosupbnd1lem1  27628  noinfcbv  27637  noinfno  27638  noinfdm  27639  nocvxminlem  27697  legval  28375  legov  28376  tglineintmo  28433  tglowdim2ln  28442  ishpg  28550  lnopp2hpgb  28554  hpgerlem  28556  colopp  28560  axcontlem1  28762  numedglnl  28944  uvtxnbgrvtx  29193  cusgrres  29249  wspniunwspnon  29721  rusgrnumwwlkb0  29769  frgr3vlem2  30071  3vfriswmgrlem  30074  fusgr2wsp2nb  30131  numclwlk2lem2f1o  30176  lpni  30277  pjhthmo  31099  chscllem2  31435  cbvdisjf  32346  2ndresdju  32418  fmptcof2  32426  aciunf1lem  32431  funcnv4mpt  32438  suppovss  32448  fpwrelmapffslem  32498  fsumiunle  32574  elrspunsn  33080  fedgmullem1  33259  zarclssn  33410  esumcvg  33641  fiunelros  33729  measiun  33773  bnj1146  34358  bnj1185  34360  bnj1385  34399  bnj1014  34528  bnj1112  34550  bnj1123  34553  bnj1228  34578  bnj1326  34593  bnj1321  34594  bnj1384  34599  bnj1417  34608  bnj1497  34627  gonarlem  34940  goalrlem  34942  goalr  34943  mrsubrn  35059  dfon2lem6  35320  dfbigcup2  35431  lineintmo  35689  eleq2w2ALT  36462  bj-idres  36575  mptsnunlem  36753  ptrest  37027  poimirlem25  37053  mblfinlem2  37066  mblfinlem3  37067  mblfinlem4  37068  ismblfin  37069  mbfposadd  37075  itg2addnclem  37079  ftc1anclem5  37105  ftc1anclem6  37106  ftc1anclem7  37107  ftc1anc  37109  areacirclem5  37120  fdc1  37154  inxprnres  37700  fsumshftd  38361  pmapglb  39180  polval2N  39316  osumcllem4N  39369  pexmidlem1N  39380  dih1dimatlem  40739  mapdh9a  41199  mapdh9aOLDN  41200  sticksstones2  41551  selvvvval  41740  fsuppind  41745  elrab2w  42014  fphpd  42158  fphpdo  42159  pellex  42177  setindtrs  42368  dford3lem2  42370  fnwe2lem2  42397  mendlmod  42539  cantnfub  42673  tfsconcat0i  42697  rababg  42927  fsovrfovd  43362  fsovcnvlem  43366  scottabf  43600  elunif  44301  iunincfi  44383  cbvmpo2  44386  cbvmpo1  44387  disjf1  44479  wessf1ornlem  44481  disjinfi  44488  supxrleubrnmptf  44756  monoordxr  44788  monoord2xr  44790  fsummulc1f  44882  fsumnncl  44883  fsumf1of  44885  fsumiunss  44886  fsumreclf  44887  fsumlessf  44888  fsumsermpt  44890  fmulcl  44892  fmul01lt1lem2  44896  fprodexp  44905  fprodabs2  44906  climmulf  44915  climexp  44916  climrecf  44920  climinff  44922  climaddf  44926  mullimc  44927  limcperiod  44939  sumnnodd  44941  neglimc  44958  addlimc  44959  climsubmpt  44971  climreclf  44975  climeldmeqmpt  44979  climfveqmpt  44982  fnlimfvre  44985  climfveqf  44991  climfveqmpt3  44993  climeldmeqf  44994  climeqf  44999  climeldmeqmpt3  45000  climinf2  45018  limsupequz  45034  limsupequzmptf  45042  lmbr3  45058  cnrefiisp  45141  cncfshift  45185  fprodcncf  45211  dvmptmulf  45248  dvmptfprod  45256  dvnprodlem1  45257  dvnprodlem3  45259  stoweidlem16  45327  stoweidlem34  45345  stoweidlem62  45373  dirkercncflem2  45415  fourierdlem12  45430  fourierdlem15  45433  fourierdlem34  45452  fourierdlem50  45467  fourierdlem73  45490  fourierdlem94  45511  fourierdlem112  45529  fourierdlem113  45530  intsaluni  45640  sge0lempt  45721  sge0iunmptlemfi  45724  sge0iunmptlemre  45726  sge0iunmpt  45729  sge0ltfirpmpt2  45737  sge0isummpt2  45743  sge0xaddlem2  45745  sge0xadd  45746  meadjiun  45777  voliunsge0lem  45783  meaiuninclem  45791  meaiunincf  45794  meaiuninc3v  45795  meaiuninc3  45796  meaiininclem  45797  meaiininc  45798  isomennd  45842  ovn0lem  45876  sge0hsphoire  45900  hoidmvlelem1  45906  hoidmvlelem2  45907  hoidmvlelem3  45908  hoidmvlelem5  45910  hspmbllem2  45938  hoimbl2  45976  vonhoire  45983  vonioo  45993  vonicc  45996  vonn0ioo2  46001  vonn0icc2  46003  pimincfltioc  46027  salpreimagtlt  46041  smflimlem4  46085  rexrsb  46403  ichexmpl2  46733  ichnreuop  46735  sbgoldbm  47047  bgoldbnnsum3prm  47067  tgoldbach  47080  srhmsubcALTV  47310  cbvmpox2  47322  mo0sn  47809  f1omo  47836  isthincd2lem1  47956  thincmo  47958