Theorem eleq1w 2811

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

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

This theorem is referenced by:  clelsb1  2855  cleqh  2857  nfcjust  2877  nfcr  2881  cleqf  2920  rspw  3212  cbvralvw  3213  cbvrexvw  3214  cbvralfw  3276  cbvralsvw  3287  cbvralf  3331  ralcom2  3348  moel  3373  cbvrmovw  3374  cbvreuvw  3375  cbvrmow  3378  cbvreu  3394  cbvrabv  3413  rabrabi  3422  cbvrabw  3438  cbvrabwOLD  3439  nfrab  3442  cbvrab  3443  elrab2w  3660  reu2  3693  reu6  3694  rmo4  3698  reu8  3701  2reu5  3726  ruOLD  3749  csbied  3895  difjust  3913  unjust  3915  injust  3917  dfss2  3929  dfssf  3934  dfdif3OLD  4077  eqeuel  4324  rabeq0w  4346  disj  4409  reldisj  4412  ralidmw  4467  dfif6  4487  rabsnifsb  4682  eluniab  4881  unissb  4899  elintabOLD  4919  uniintsn  4945  dfiun2g  4990  dfiunv2  4994  disjxun  5100  cbvmptf  5202  cbvmptfg  5203  cbvmptv  5206  dftr2c  5212  isso2i  5576  dfres2  6001  imai  6034  frpoinsg  6304  tz7.7  6346  fvn0ssdmfun  7028  fmptco  7083  cbvriotaw  7335  cbvriotavw  7336  cbvriota  7339  cbvmpox  7462  cbvmpov  7464  tfis  7811  tfindes  7819  peano5  7849  findes  7856  dfoprab4f  8014  fmpox  8025  xpord2indlem  8103  poseq  8114  soseq  8115  smogt  8313  resixpfo  8886  ixpsnf1o  8888  dom2lem  8940  mapsnend  8984  pw2f1olem  9022  pssnn  9109  ssfi  9114  findcard3  9205  findcard3OLD  9206  ordiso2  9444  elirrv  9525  cantnflem1d  9617  cantnf  9622  setind  9663  frinsg  9680  tz9.12lem3  9718  infxpen  9943  dfac5lem4  10055  dfac12lem2  10074  kmlem14  10093  cfsmolem  10199  sornom  10206  isf32lem9  10290  axdc2  10378  fpwwe2lem7  10566  fpwwe2  10572  wunex2  10667  dedekindle  11314  wloglei  11686  uzind4s  12843  seqof2  14001  reuccatpfxs1  14688  shftfn  15015  rexuz3  15291  zsum  15660  fsum  15662  sumss  15666  sumss2  15668  fsumcvg2  15669  fsumser  15672  fsumclf  15680  fsumsplitf  15684  isumless  15787  prodfdiv  15838  cbvprod  15855  cbvprodv  15856  zprod  15879  fprod  15883  fprodntriv  15884  prodss  15889  fprod2dlem  15922  fproddivf  15929  fprodsplitf  15930  rpnnen2lem10  16167  cpnnen  16173  sumeven  16333  sumodd  16334  sadcp1  16401  smupp1  16426  pcmptdvds  16841  prmreclem2  16864  prmreclem5  16867  prmreclem6  16868  prmrec  16869  prmdvdsprmo  16989  iscatd2  17622  initoeu2  17958  yoniso  18226  sgrpidmnd  18648  mndind  18737  eqg0subg  19110  symggen  19384  dprd2d2  19960  srhmsubc  20600  isdrngrd  20686  isdrngrdOLD  20688  lbspss  21021  frlmphl  21723  frlmup1  21740  opsrtoslem1  21995  mdetralt  22528  mdetralt2  22529  mdetunilem2  22533  maducoeval2  22560  chfacfscmulgsum  22780  chfacfpmmulgsum  22784  isclo2  23008  neiptopnei  23052  ptcldmpt  23534  elmptrab  23747  hausflimi  23900  hausflim  23901  alexsubALTlem3  23969  alexsubALTlem4  23970  ptcmplem2  23973  cnextcn  23987  cnextfres1  23988  tgphaus  24037  ustuqtop  24167  utopsnneip  24169  ucncn  24205  nrmmetd  24495  xrhmeo  24877  iscau2  25210  caucfil  25216  cmetcaulem  25221  bcth  25262  vitalilem3  25544  vitali  25547  i1f1lem  25623  itg11  25625  i1fres  25639  mbfi1fseq  25655  mbfi1flim  25657  itg2uba  25677  itg2splitlem  25682  isibl2  25700  cbvitg  25710  cbvitgv  25711  itgss3  25749  dvmptfsum  25912  rolle  25927  elply2  26134  plyexmo  26254  lgamgulmlem2  26973  prmorcht  27121  pclogsum  27159  dchr1  27201  lgsdir  27276  lgsdilem2  27277  lgsdi  27278  lgsne0  27279  lgsquadlem3  27326  lgsquad  27327  2sqlem8  27370  nosupcbv  27647  nosupno  27648  nosupdm  27649  nosupbnd1lem1  27653  noinfcbv  27662  noinfno  27663  noinfdm  27664  nocvxminlem  27723  legval  28564  legov  28565  tglineintmo  28622  tglowdim2ln  28631  ishpg  28739  lnopp2hpgb  28743  hpgerlem  28745  colopp  28749  axcontlem1  28944  numedglnl  29124  uvtxnbgrvtx  29373  cusgrres  29429  wspniunwspnon  29903  rusgrnumwwlkb0  29951  frgr3vlem2  30253  3vfriswmgrlem  30256  fusgr2wsp2nb  30313  numclwlk2lem2f1o  30358  lpni  30459  pjhthmo  31281  chscllem2  31617  cbvdisjf  32550  2ndresdju  32623  fmptcof2  32631  aciunf1lem  32636  funcnv4mpt  32643  suppovss  32654  fpwrelmapffslem  32705  fsumiunle  32804  gsumwrd2dccatlem  33049  elrspunsn  33393  1arithufdlem3  33510  fedgmullem1  33618  fldextrspunlsp  33662  zarclssn  33856  esumcvg  34069  fiunelros  34157  measiun  34201  bnj1146  34774  bnj1185  34776  bnj1385  34815  bnj1014  34944  bnj1112  34966  bnj1123  34969  bnj1228  34994  bnj1326  35009  bnj1321  35010  bnj1384  35015  bnj1417  35024  bnj1497  35043  onvf1odlem2  35084  onvf1odlem3  35085  gonarlem  35374  goalrlem  35376  goalr  35377  mrsubrn  35493  dfon2lem6  35769  dfbigcup2  35880  lineintmo  36138  cbvralvw2  36207  cbvrexvw2  36208  cbvrmovw2  36209  cbvreuvw2  36210  cbvmptvw2  36215  cbvprodvw2  36228  cbvrmodavw  36233  cbvreudavw  36234  cbvrabdavw  36242  cbvmptdavw  36248  cbvriotadavw  36251  cbvixpdavw  36259  cbvproddavw  36261  cbvitgdavw  36262  cbvrabdavw2  36266  cbvmptdavw2  36269  cbvriotadavw2  36271  weiunlem2  36444  eleq2w2ALT  37028  bj-idres  37141  mptsnunlem  37319  ptrest  37606  poimirlem25  37632  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  mbfposadd  37654  itg2addnclem  37658  ftc1anclem5  37684  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anc  37688  areacirclem5  37699  fdc1  37733  inxprnres  38273  fsumshftd  38938  pmapglb  39757  polval2N  39893  osumcllem4N  39946  pexmidlem1N  39957  dih1dimatlem  41316  mapdh9a  41776  mapdh9aOLDN  41777  sticksstones2  42128  selvvvval  42566  fsuppind  42571  fphpd  42797  fphpdo  42798  pellex  42816  setindtrs  43007  dford3lem2  43009  fnwe2lem2  43033  mendlmod  43171  cantnfub  43303  tfsconcat0i  43327  rababg  43556  fsovrfovd  43991  fsovcnvlem  43995  scottabf  44222  trfr  44945  elunif  45003  iunincfi  45081  cbvmpo2  45084  cbvmpo1  45085  disjf1  45170  wessf1ornlem  45172  disjinfi  45179  supxrleubrnmptf  45440  monoordxr  45471  monoord2xr  45473  fsummulc1f  45562  fsumnncl  45563  fsumf1of  45565  fsumiunss  45566  fsumreclf  45567  fsumlessf  45568  fsumsermpt  45570  fmulcl  45572  fmul01lt1lem2  45576  fprodexp  45585  fprodabs2  45586  climmulf  45595  climexp  45596  climrecf  45600  climinff  45602  climaddf  45606  mullimc  45607  limcperiod  45619  sumnnodd  45621  neglimc  45638  addlimc  45639  climsubmpt  45651  climreclf  45655  climeldmeqmpt  45659  climfveqmpt  45662  fnlimfvre  45665  climfveqf  45671  climfveqmpt3  45673  climeldmeqf  45674  climeqf  45679  climeldmeqmpt3  45680  climinf2  45698  limsupequz  45714  limsupequzmptf  45722  lmbr3  45738  cnrefiisp  45821  cncfshift  45865  fprodcncf  45891  dvmptmulf  45928  dvmptfprod  45936  dvnprodlem1  45937  dvnprodlem3  45939  stoweidlem16  46007  stoweidlem34  46025  stoweidlem62  46053  dirkercncflem2  46095  fourierdlem12  46110  fourierdlem15  46113  fourierdlem34  46132  fourierdlem50  46147  fourierdlem73  46170  fourierdlem94  46191  fourierdlem112  46209  fourierdlem113  46210  intsaluni  46320  sge0lempt  46401  sge0iunmptlemfi  46404  sge0iunmptlemre  46406  sge0iunmpt  46409  sge0ltfirpmpt2  46417  sge0isummpt2  46423  sge0xaddlem2  46425  sge0xadd  46426  meadjiun  46457  voliunsge0lem  46463  meaiuninclem  46471  meaiunincf  46474  meaiuninc3v  46475  meaiuninc3  46476  meaiininclem  46477  meaiininc  46478  isomennd  46522  ovn0lem  46556  sge0hsphoire  46580  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem5  46590  hspmbllem2  46618  hoimbl2  46656  vonhoire  46663  vonioo  46673  vonicc  46676  vonn0ioo2  46681  vonn0icc2  46683  pimincfltioc  46707  salpreimagtlt  46721  smflimlem4  46765  ormkglobd  46866  sinnpoly  46885  rexrsb  47094  ichexmpl2  47464  ichnreuop  47466  sbgoldbm  47778  bgoldbnnsum3prm  47798  tgoldbach  47811  srhmsubcALTV  48306  cbvmpox2  48317  mo0sn  48797  f1omoOLD  48875  isthincd2lem1  49407  thincmo  49410  euendfunc  49508