Theorem eleq1w 2820

Description: Weaker version of eleq1 2825 (but more general than elequ1 2121) not depending on ax-ext 2709 nor df-cleq 2729.

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  clelsb1  2864  cleqh  2866  nfcjust  2885  nfcr  2889  cleqf  2928  rspw  3215  cbvralvw  3216  cbvrexvw  3217  cbvralfw  3278  cbvralsvw  3289  cbvralf  3332  ralcom2  3349  moel  3372  cbvrmovw  3373  cbvreuvw  3374  cbvrmow  3377  cbvreu  3393  cbvrabv  3411  rabrabi  3420  cbvrabw  3436  cbvrabwOLD  3437  nfrab  3440  cbvrab  3441  elrab2w  3652  reu2  3685  reu6  3686  rmo4  3690  reu8  3693  2reu5  3718  ruOLD  3741  csbied  3887  difjust  3905  unjust  3907  injust  3909  dfss2  3921  dfssf  3926  dfdif3OLD  4072  eqeuel  4319  rabeq0w  4341  disj  4404  reldisj  4407  ralidmw  4471  dfif6  4484  rabsnifsb  4681  eluniab  4879  unissb  4898  uniintsn  4942  dfiun2g  4987  dfiunv2  4991  disjxun  5098  cbvmptf  5200  cbvmptfg  5201  cbvmptv  5204  dftr2c  5210  isso2i  5577  dfres2  6008  imai  6041  frpoinsg  6309  tz7.7  6351  fvn0ssdmfun  7028  fmptco  7084  cbvriotaw  7334  cbvriotavw  7335  cbvriota  7338  cbvmpox  7461  cbvmpov  7463  tfis  7807  tfindes  7815  peano5  7845  findes  7852  dfoprab4f  8010  fmpox  8021  xpord2indlem  8099  poseq  8110  soseq  8111  smogt  8309  resixpfo  8886  ixpsnf1o  8888  dom2lem  8941  mapsnend  8985  pw2f1olem  9021  pssnn  9105  ssfi  9109  findcard3  9195  ordiso2  9432  elirrvOLD  9515  cantnflem1d  9609  cantnf  9614  setind  9668  frinsg  9675  tz9.12lem3  9713  infxpen  9936  dfac5lem4  10048  dfac12lem2  10067  kmlem14  10086  cfsmolem  10192  sornom  10199  isf32lem9  10283  axdc2  10371  fpwwe2lem7  10560  fpwwe2  10566  wunex2  10661  dedekindle  11309  wloglei  11681  uzind4s  12833  seqof2  13995  reuccatpfxs1  14682  shftfn  15008  rexuz3  15284  zsum  15653  fsum  15655  sumss  15659  sumss2  15661  fsumcvg2  15662  fsumser  15665  fsumclf  15673  fsumsplitf  15677  isumless  15780  prodfdiv  15831  cbvprod  15848  cbvprodv  15849  zprod  15872  fprod  15876  fprodntriv  15877  prodss  15882  fprod2dlem  15915  fproddivf  15922  fprodsplitf  15923  rpnnen2lem10  16160  cpnnen  16166  sumeven  16326  sumodd  16327  sadcp1  16394  smupp1  16419  pcmptdvds  16834  prmreclem2  16857  prmreclem5  16860  prmreclem6  16861  prmrec  16862  prmdvdsprmo  16982  iscatd2  17616  initoeu2  17952  yoniso  18220  sgrpidmnd  18676  mndind  18765  eqg0subg  19137  symggen  19411  dprd2d2  19987  srhmsubc  20625  isdrngrd  20711  isdrngrdOLD  20713  lbspss  21046  frlmphl  21748  frlmup1  21765  opsrtoslem1  22022  mdetralt  22564  mdetralt2  22565  mdetunilem2  22569  maducoeval2  22596  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  isclo2  23044  neiptopnei  23088  ptcldmpt  23570  elmptrab  23783  hausflimi  23936  hausflim  23937  alexsubALTlem3  24005  alexsubALTlem4  24006  ptcmplem2  24009  cnextcn  24023  cnextfres1  24024  tgphaus  24073  ustuqtop  24202  utopsnneip  24204  ucncn  24240  nrmmetd  24530  xrhmeo  24912  iscau2  25245  caucfil  25251  cmetcaulem  25256  bcth  25297  vitalilem3  25579  vitali  25582  i1f1lem  25658  itg11  25660  i1fres  25674  mbfi1fseq  25690  mbfi1flim  25692  itg2uba  25712  itg2splitlem  25717  isibl2  25735  cbvitg  25745  cbvitgv  25746  itgss3  25784  dvmptfsum  25947  rolle  25962  elply2  26169  plyexmo  26289  lgamgulmlem2  27008  prmorcht  27156  pclogsum  27194  dchr1  27236  lgsdir  27311  lgsdilem2  27312  lgsdi  27313  lgsne0  27314  lgsquadlem3  27361  lgsquad  27362  2sqlem8  27405  nosupcbv  27682  nosupno  27683  nosupdm  27684  nosupbnd1lem1  27688  noinfcbv  27697  noinfno  27698  noinfdm  27699  nocvxminlem  27762  legval  28668  legov  28669  tglineintmo  28726  tglowdim2ln  28735  ishpg  28843  lnopp2hpgb  28847  hpgerlem  28849  colopp  28853  axcontlem1  29049  numedglnl  29229  uvtxnbgrvtx  29478  cusgrres  29534  wspniunwspnon  30008  rusgrnumwwlkb0  30059  frgr3vlem2  30361  3vfriswmgrlem  30364  fusgr2wsp2nb  30421  numclwlk2lem2f1o  30466  lpni  30568  pjhthmo  31390  chscllem2  31726  cbvdisjf  32658  2ndresdju  32739  fmptcof2  32747  aciunf1lem  32752  funcnv4mpt  32758  suppovss  32771  fpwrelmapffslem  32822  fsumiunle  32921  gsumwrd2dccatlem  33171  elrspunsn  33522  1arithufdlem3  33639  fedgmullem1  33807  fldextrspunlsp  33852  extdgfialglem2  33871  zarclssn  34051  esumcvg  34264  fiunelros  34352  measiun  34396  bnj1146  34967  bnj1185  34969  bnj1385  35008  bnj1014  35137  bnj1112  35159  bnj1123  35162  bnj1228  35187  bnj1326  35202  bnj1321  35203  bnj1384  35208  bnj1417  35217  bnj1497  35236  trssfir1om  35289  r1omhfb  35290  fineqvnttrclse  35302  axregscl  35306  setindregs  35308  trssfir1omregs  35314  r1omhfbregs  35315  onvf1odlem2  35320  onvf1odlem3  35321  gonarlem  35610  goalrlem  35612  goalr  35613  mrsubrn  35729  dfon2lem6  36002  dfbigcup2  36113  lineintmo  36373  cbvralvw2  36442  cbvrexvw2  36443  cbvrmovw2  36444  cbvreuvw2  36445  cbvmptvw2  36450  cbvprodvw2  36463  cbvrmodavw  36468  cbvreudavw  36469  cbvrabdavw  36477  cbvmptdavw  36483  cbvriotadavw  36486  cbvixpdavw  36494  cbvproddavw  36496  cbvitgdavw  36497  cbvrabdavw2  36501  cbvmptdavw2  36504  cbvriotadavw2  36506  weiunlem  36679  eleq2w2ALT  37295  bj-idres  37415  mptsnunlem  37593  ptrest  37870  poimirlem25  37896  mblfinlem2  37909  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  mbfposadd  37918  itg2addnclem  37922  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anclem7  37950  ftc1anc  37952  areacirclem5  37963  fdc1  37997  inxprnres  38549  fsumshftd  39328  pmapglb  40146  polval2N  40282  osumcllem4N  40335  pexmidlem1N  40346  dih1dimatlem  41705  mapdh9a  42165  mapdh9aOLDN  42166  sticksstones2  42517  selvvvval  42943  fsuppind  42948  fphpd  43173  fphpdo  43174  pellex  43192  setindtrs  43382  dford3lem2  43384  fnwe2lem2  43408  mendlmod  43546  cantnfub  43678  tfsconcat0i  43702  rababg  43930  fsovrfovd  44365  fsovcnvlem  44369  scottabf  44596  trfr  45318  elunif  45376  iunincfi  45453  cbvmpo2  45456  cbvmpo1  45457  disjf1  45542  wessf1ornlem  45544  disjinfi  45551  supxrleubrnmptf  45809  monoordxr  45840  monoord2xr  45842  fsummulc1f  45931  fsumnncl  45932  fsumf1of  45934  fsumiunss  45935  fsumreclf  45936  fsumlessf  45937  fsumsermpt  45939  fmulcl  45941  fmul01lt1lem2  45945  fprodexp  45954  fprodabs2  45955  climmulf  45964  climexp  45965  climrecf  45969  climinff  45971  climaddf  45975  mullimc  45976  limcperiod  45988  sumnnodd  45990  neglimc  46005  addlimc  46006  climsubmpt  46018  climreclf  46022  climeldmeqmpt  46026  climfveqmpt  46029  fnlimfvre  46032  climfveqf  46038  climfveqmpt3  46040  climeldmeqf  46041  climeqf  46046  climeldmeqmpt3  46047  climinf2  46065  limsupequz  46081  limsupequzmptf  46089  lmbr3  46105  cnrefiisp  46188  cncfshift  46232  fprodcncf  46258  dvmptmulf  46295  dvmptfprod  46303  dvnprodlem1  46304  dvnprodlem3  46306  stoweidlem16  46374  stoweidlem34  46392  stoweidlem62  46420  dirkercncflem2  46462  fourierdlem12  46477  fourierdlem15  46480  fourierdlem34  46499  fourierdlem50  46514  fourierdlem73  46537  fourierdlem94  46558  fourierdlem112  46576  fourierdlem113  46577  intsaluni  46687  sge0lempt  46768  sge0iunmptlemfi  46771  sge0iunmptlemre  46773  sge0iunmpt  46776  sge0ltfirpmpt2  46784  sge0isummpt2  46790  sge0xaddlem2  46792  sge0xadd  46793  meadjiun  46824  voliunsge0lem  46830  meaiuninclem  46838  meaiunincf  46841  meaiuninc3v  46842  meaiuninc3  46843  meaiininclem  46844  meaiininc  46845  isomennd  46889  ovn0lem  46923  sge0hsphoire  46947  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem5  46957  hspmbllem2  46985  hoimbl2  47023  vonhoire  47030  vonioo  47040  vonicc  47043  vonn0ioo2  47048  vonn0icc2  47050  pimincfltioc  47074  salpreimagtlt  47088  smflimlem4  47132  ormkglobd  47233  sinnpoly  47251  rexrsb  47460  ichexmpl2  47830  ichnreuop  47832  sbgoldbm  48144  bgoldbnnsum3prm  48164  tgoldbach  48177  srhmsubcALTV  48685  cbvmpox2  48696  mo0sn  49175  f1omoOLD  49253  isthincd2lem1  49784  thincmo  49787  euendfunc  49885