Theorem eleq1w 2812

Description: Weaker version of eleq1 2817 (but more general than elequ1 2116) not depending on ax-ext 2702 nor df-cleq 2722.

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804

This theorem is referenced by:  clelsb1  2856  cleqh  2858  nfcjust  2878  nfcr  2882  cleqf  2921  rspw  3215  cbvralvw  3216  cbvrexvw  3217  cbvralfw  3280  cbvralsvw  3292  cbvralf  3336  ralcom2  3353  moel  3378  cbvrmovw  3379  cbvreuvw  3380  cbvrmow  3383  cbvreuwOLD  3389  cbvreu  3400  cbvrabv  3419  rabrabi  3428  cbvrabw  3444  cbvrabwOLD  3445  nfrab  3448  cbvrab  3449  elrab2w  3666  reu2  3699  reu6  3700  rmo4  3704  reu8  3707  2reu5  3732  ruOLD  3755  csbied  3901  difjust  3919  unjust  3921  injust  3923  dfss2  3935  dfssf  3940  dfdif3OLD  4084  eqeuel  4331  rabeq0w  4353  disj  4416  reldisj  4419  ralidmw  4474  dfif6  4494  rabsnifsb  4689  eluniab  4888  unissb  4906  elintabOLD  4926  uniintsn  4952  dfiun2g  4997  dfiunv2  5002  disjxun  5108  cbvmptf  5210  cbvmptfg  5211  cbvmptv  5214  dftr2c  5220  isso2i  5586  dfres2  6015  imai  6048  frpoinsg  6319  tz7.7  6361  fvn0ssdmfun  7049  fmptco  7104  cbvriotaw  7356  cbvriotavw  7357  cbvriota  7360  cbvmpox  7485  cbvmpov  7487  tfis  7834  tfindes  7842  peano5  7872  findes  7879  dfoprab4f  8038  fmpox  8049  xpord2indlem  8129  poseq  8140  soseq  8141  smogt  8339  resixpfo  8912  ixpsnf1o  8914  dom2lem  8966  mapsnend  9010  pw2f1olem  9050  pssnn  9138  ssfi  9143  findcard3  9236  findcard3OLD  9237  ordiso2  9475  elirrv  9556  cantnflem1d  9648  cantnf  9653  setind  9694  frinsg  9711  tz9.12lem3  9749  infxpen  9974  dfac5lem4  10086  dfac12lem2  10105  kmlem14  10124  cfsmolem  10230  sornom  10237  isf32lem9  10321  axdc2  10409  fpwwe2lem7  10597  fpwwe2  10603  wunex2  10698  dedekindle  11345  wloglei  11717  uzind4s  12874  seqof2  14032  reuccatpfxs1  14719  shftfn  15046  rexuz3  15322  zsum  15691  fsum  15693  sumss  15697  sumss2  15699  fsumcvg2  15700  fsumser  15703  fsumclf  15711  fsumsplitf  15715  isumless  15818  prodfdiv  15869  cbvprod  15886  cbvprodv  15887  zprod  15910  fprod  15914  fprodntriv  15915  prodss  15920  fprod2dlem  15953  fproddivf  15960  fprodsplitf  15961  rpnnen2lem10  16198  cpnnen  16204  sumeven  16364  sumodd  16365  sadcp1  16432  smupp1  16457  pcmptdvds  16872  prmreclem2  16895  prmreclem5  16898  prmreclem6  16899  prmrec  16900  prmdvdsprmo  17020  iscatd2  17649  initoeu2  17985  yoniso  18253  sgrpidmnd  18673  mndind  18762  eqg0subg  19135  symggen  19407  dprd2d2  19983  srhmsubc  20596  isdrngrd  20682  isdrngrdOLD  20684  lbspss  20996  frlmphl  21697  frlmup1  21714  opsrtoslem1  21969  mdetralt  22502  mdetralt2  22503  mdetunilem2  22507  maducoeval2  22534  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  isclo2  22982  neiptopnei  23026  ptcldmpt  23508  elmptrab  23721  hausflimi  23874  hausflim  23875  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem2  23947  cnextcn  23961  cnextfres1  23962  tgphaus  24011  ustuqtop  24141  utopsnneip  24143  ucncn  24179  nrmmetd  24469  xrhmeo  24851  iscau2  25184  caucfil  25190  cmetcaulem  25195  bcth  25236  vitalilem3  25518  vitali  25521  i1f1lem  25597  itg11  25599  i1fres  25613  mbfi1fseq  25629  mbfi1flim  25631  itg2uba  25651  itg2splitlem  25656  isibl2  25674  cbvitg  25684  cbvitgv  25685  itgss3  25723  dvmptfsum  25886  rolle  25901  elply2  26108  plyexmo  26228  lgamgulmlem2  26947  prmorcht  27095  pclogsum  27133  dchr1  27175  lgsdir  27250  lgsdilem2  27251  lgsdi  27252  lgsne0  27253  lgsquadlem3  27300  lgsquad  27301  2sqlem8  27344  nosupcbv  27621  nosupno  27622  nosupdm  27623  nosupbnd1lem1  27627  noinfcbv  27636  noinfno  27637  noinfdm  27638  nocvxminlem  27696  legval  28518  legov  28519  tglineintmo  28576  tglowdim2ln  28585  ishpg  28693  lnopp2hpgb  28697  hpgerlem  28699  colopp  28703  axcontlem1  28898  numedglnl  29078  uvtxnbgrvtx  29327  cusgrres  29383  wspniunwspnon  29860  rusgrnumwwlkb0  29908  frgr3vlem2  30210  3vfriswmgrlem  30213  fusgr2wsp2nb  30270  numclwlk2lem2f1o  30315  lpni  30416  pjhthmo  31238  chscllem2  31574  cbvdisjf  32507  2ndresdju  32580  fmptcof2  32588  aciunf1lem  32593  funcnv4mpt  32600  suppovss  32611  fpwrelmapffslem  32662  fsumiunle  32761  gsumwrd2dccatlem  33013  elrspunsn  33407  1arithufdlem3  33524  fedgmullem1  33632  fldextrspunlsp  33676  zarclssn  33870  esumcvg  34083  fiunelros  34171  measiun  34215  bnj1146  34788  bnj1185  34790  bnj1385  34829  bnj1014  34958  bnj1112  34980  bnj1123  34983  bnj1228  35008  bnj1326  35023  bnj1321  35024  bnj1384  35029  bnj1417  35038  bnj1497  35057  onvf1odlem2  35098  onvf1odlem3  35099  gonarlem  35388  goalrlem  35390  goalr  35391  mrsubrn  35507  dfon2lem6  35783  dfbigcup2  35894  lineintmo  36152  cbvralvw2  36221  cbvrexvw2  36222  cbvrmovw2  36223  cbvreuvw2  36224  cbvmptvw2  36229  cbvprodvw2  36242  cbvrmodavw  36247  cbvreudavw  36248  cbvrabdavw  36256  cbvmptdavw  36262  cbvriotadavw  36265  cbvixpdavw  36273  cbvproddavw  36275  cbvitgdavw  36276  cbvrabdavw2  36280  cbvmptdavw2  36283  cbvriotadavw2  36285  weiunlem2  36458  eleq2w2ALT  37042  bj-idres  37155  mptsnunlem  37333  ptrest  37620  poimirlem25  37646  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  mbfposadd  37668  itg2addnclem  37672  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anc  37702  areacirclem5  37713  fdc1  37747  inxprnres  38287  fsumshftd  38952  pmapglb  39771  polval2N  39907  osumcllem4N  39960  pexmidlem1N  39971  dih1dimatlem  41330  mapdh9a  41790  mapdh9aOLDN  41791  sticksstones2  42142  selvvvval  42580  fsuppind  42585  fphpd  42811  fphpdo  42812  pellex  42830  setindtrs  43021  dford3lem2  43023  fnwe2lem2  43047  mendlmod  43185  cantnfub  43317  tfsconcat0i  43341  rababg  43570  fsovrfovd  44005  fsovcnvlem  44009  scottabf  44236  trfr  44959  elunif  45017  iunincfi  45095  cbvmpo2  45098  cbvmpo1  45099  disjf1  45184  wessf1ornlem  45186  disjinfi  45193  supxrleubrnmptf  45454  monoordxr  45485  monoord2xr  45487  fsummulc1f  45576  fsumnncl  45577  fsumf1of  45579  fsumiunss  45580  fsumreclf  45581  fsumlessf  45582  fsumsermpt  45584  fmulcl  45586  fmul01lt1lem2  45590  fprodexp  45599  fprodabs2  45600  climmulf  45609  climexp  45610  climrecf  45614  climinff  45616  climaddf  45620  mullimc  45621  limcperiod  45633  sumnnodd  45635  neglimc  45652  addlimc  45653  climsubmpt  45665  climreclf  45669  climeldmeqmpt  45673  climfveqmpt  45676  fnlimfvre  45679  climfveqf  45685  climfveqmpt3  45687  climeldmeqf  45688  climeqf  45693  climeldmeqmpt3  45694  climinf2  45712  limsupequz  45728  limsupequzmptf  45736  lmbr3  45752  cnrefiisp  45835  cncfshift  45879  fprodcncf  45905  dvmptmulf  45942  dvmptfprod  45950  dvnprodlem1  45951  dvnprodlem3  45953  stoweidlem16  46021  stoweidlem34  46039  stoweidlem62  46067  dirkercncflem2  46109  fourierdlem12  46124  fourierdlem15  46127  fourierdlem34  46146  fourierdlem50  46161  fourierdlem73  46184  fourierdlem94  46205  fourierdlem112  46223  fourierdlem113  46224  intsaluni  46334  sge0lempt  46415  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0ltfirpmpt2  46431  sge0isummpt2  46437  sge0xaddlem2  46439  sge0xadd  46440  meadjiun  46471  voliunsge0lem  46477  meaiuninclem  46485  meaiunincf  46488  meaiuninc3v  46489  meaiuninc3  46490  meaiininclem  46491  meaiininc  46492  isomennd  46536  ovn0lem  46570  sge0hsphoire  46594  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem5  46604  hspmbllem2  46632  hoimbl2  46670  vonhoire  46677  vonioo  46687  vonicc  46690  vonn0ioo2  46695  vonn0icc2  46697  pimincfltioc  46721  salpreimagtlt  46735  smflimlem4  46779  ormkglobd  46880  rexrsb  47105  ichexmpl2  47475  ichnreuop  47477  sbgoldbm  47789  bgoldbnnsum3prm  47809  tgoldbach  47822  srhmsubcALTV  48317  cbvmpox2  48328  mo0sn  48808  f1omoOLD  48886  isthincd2lem1  49418  thincmo  49421  euendfunc  49519