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  3214  cbvralvw  3215  cbvrexvw  3216  cbvralfw  3278  cbvralsvw  3290  cbvralf  3334  ralcom2  3351  moel  3376  cbvrmovw  3377  cbvreuvw  3378  cbvrmow  3381  cbvreu  3397  cbvrabv  3416  rabrabi  3425  cbvrabw  3441  cbvrabwOLD  3442  nfrab  3445  cbvrab  3446  elrab2w  3663  reu2  3696  reu6  3697  rmo4  3701  reu8  3704  2reu5  3729  ruOLD  3752  csbied  3898  difjust  3916  unjust  3918  injust  3920  dfss2  3932  dfssf  3937  dfdif3OLD  4081  eqeuel  4328  rabeq0w  4350  disj  4413  reldisj  4416  ralidmw  4471  dfif6  4491  rabsnifsb  4686  eluniab  4885  unissb  4903  elintabOLD  4923  uniintsn  4949  dfiun2g  4994  dfiunv2  4999  disjxun  5105  cbvmptf  5207  cbvmptfg  5208  cbvmptv  5211  dftr2c  5217  isso2i  5583  dfres2  6012  imai  6045  frpoinsg  6316  tz7.7  6358  fvn0ssdmfun  7046  fmptco  7101  cbvriotaw  7353  cbvriotavw  7354  cbvriota  7357  cbvmpox  7482  cbvmpov  7484  tfis  7831  tfindes  7839  peano5  7869  findes  7876  dfoprab4f  8035  fmpox  8046  xpord2indlem  8126  poseq  8137  soseq  8138  smogt  8336  resixpfo  8909  ixpsnf1o  8911  dom2lem  8963  mapsnend  9007  pw2f1olem  9045  pssnn  9132  ssfi  9137  findcard3  9229  findcard3OLD  9230  ordiso2  9468  elirrv  9549  cantnflem1d  9641  cantnf  9646  setind  9687  frinsg  9704  tz9.12lem3  9742  infxpen  9967  dfac5lem4  10079  dfac12lem2  10098  kmlem14  10117  cfsmolem  10223  sornom  10230  isf32lem9  10314  axdc2  10402  fpwwe2lem7  10590  fpwwe2  10596  wunex2  10691  dedekindle  11338  wloglei  11710  uzind4s  12867  seqof2  14025  reuccatpfxs1  14712  shftfn  15039  rexuz3  15315  zsum  15684  fsum  15686  sumss  15690  sumss2  15692  fsumcvg2  15693  fsumser  15696  fsumclf  15704  fsumsplitf  15708  isumless  15811  prodfdiv  15862  cbvprod  15879  cbvprodv  15880  zprod  15903  fprod  15907  fprodntriv  15908  prodss  15913  fprod2dlem  15946  fproddivf  15953  fprodsplitf  15954  rpnnen2lem10  16191  cpnnen  16197  sumeven  16357  sumodd  16358  sadcp1  16425  smupp1  16450  pcmptdvds  16865  prmreclem2  16888  prmreclem5  16891  prmreclem6  16892  prmrec  16893  prmdvdsprmo  17013  iscatd2  17642  initoeu2  17978  yoniso  18246  sgrpidmnd  18666  mndind  18755  eqg0subg  19128  symggen  19400  dprd2d2  19976  srhmsubc  20589  isdrngrd  20675  isdrngrdOLD  20677  lbspss  20989  frlmphl  21690  frlmup1  21707  opsrtoslem1  21962  mdetralt  22495  mdetralt2  22496  mdetunilem2  22500  maducoeval2  22527  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  isclo2  22975  neiptopnei  23019  ptcldmpt  23501  elmptrab  23714  hausflimi  23867  hausflim  23868  alexsubALTlem3  23936  alexsubALTlem4  23937  ptcmplem2  23940  cnextcn  23954  cnextfres1  23955  tgphaus  24004  ustuqtop  24134  utopsnneip  24136  ucncn  24172  nrmmetd  24462  xrhmeo  24844  iscau2  25177  caucfil  25183  cmetcaulem  25188  bcth  25229  vitalilem3  25511  vitali  25514  i1f1lem  25590  itg11  25592  i1fres  25606  mbfi1fseq  25622  mbfi1flim  25624  itg2uba  25644  itg2splitlem  25649  isibl2  25667  cbvitg  25677  cbvitgv  25678  itgss3  25716  dvmptfsum  25879  rolle  25894  elply2  26101  plyexmo  26221  lgamgulmlem2  26940  prmorcht  27088  pclogsum  27126  dchr1  27168  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  lgsquadlem3  27293  lgsquad  27294  2sqlem8  27337  nosupcbv  27614  nosupno  27615  nosupdm  27616  nosupbnd1lem1  27620  noinfcbv  27629  noinfno  27630  noinfdm  27631  nocvxminlem  27689  legval  28511  legov  28512  tglineintmo  28569  tglowdim2ln  28578  ishpg  28686  lnopp2hpgb  28690  hpgerlem  28692  colopp  28696  axcontlem1  28891  numedglnl  29071  uvtxnbgrvtx  29320  cusgrres  29376  wspniunwspnon  29853  rusgrnumwwlkb0  29901  frgr3vlem2  30203  3vfriswmgrlem  30206  fusgr2wsp2nb  30263  numclwlk2lem2f1o  30308  lpni  30409  pjhthmo  31231  chscllem2  31567  cbvdisjf  32500  2ndresdju  32573  fmptcof2  32581  aciunf1lem  32586  funcnv4mpt  32593  suppovss  32604  fpwrelmapffslem  32655  fsumiunle  32754  gsumwrd2dccatlem  33006  elrspunsn  33400  1arithufdlem3  33517  fedgmullem1  33625  fldextrspunlsp  33669  zarclssn  33863  esumcvg  34076  fiunelros  34164  measiun  34208  bnj1146  34781  bnj1185  34783  bnj1385  34822  bnj1014  34951  bnj1112  34973  bnj1123  34976  bnj1228  35001  bnj1326  35016  bnj1321  35017  bnj1384  35022  bnj1417  35031  bnj1497  35050  onvf1odlem2  35091  onvf1odlem3  35092  gonarlem  35381  goalrlem  35383  goalr  35384  mrsubrn  35500  dfon2lem6  35776  dfbigcup2  35887  lineintmo  36145  cbvralvw2  36214  cbvrexvw2  36215  cbvrmovw2  36216  cbvreuvw2  36217  cbvmptvw2  36222  cbvprodvw2  36235  cbvrmodavw  36240  cbvreudavw  36241  cbvrabdavw  36249  cbvmptdavw  36255  cbvriotadavw  36258  cbvixpdavw  36266  cbvproddavw  36268  cbvitgdavw  36269  cbvrabdavw2  36273  cbvmptdavw2  36276  cbvriotadavw2  36278  weiunlem2  36451  eleq2w2ALT  37035  bj-idres  37148  mptsnunlem  37326  ptrest  37613  poimirlem25  37639  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  mbfposadd  37661  itg2addnclem  37665  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anc  37695  areacirclem5  37706  fdc1  37740  inxprnres  38280  fsumshftd  38945  pmapglb  39764  polval2N  39900  osumcllem4N  39953  pexmidlem1N  39964  dih1dimatlem  41323  mapdh9a  41783  mapdh9aOLDN  41784  sticksstones2  42135  selvvvval  42573  fsuppind  42578  fphpd  42804  fphpdo  42805  pellex  42823  setindtrs  43014  dford3lem2  43016  fnwe2lem2  43040  mendlmod  43178  cantnfub  43310  tfsconcat0i  43334  rababg  43563  fsovrfovd  43998  fsovcnvlem  44002  scottabf  44229  trfr  44952  elunif  45010  iunincfi  45088  cbvmpo2  45091  cbvmpo1  45092  disjf1  45177  wessf1ornlem  45179  disjinfi  45186  supxrleubrnmptf  45447  monoordxr  45478  monoord2xr  45480  fsummulc1f  45569  fsumnncl  45570  fsumf1of  45572  fsumiunss  45573  fsumreclf  45574  fsumlessf  45575  fsumsermpt  45577  fmulcl  45579  fmul01lt1lem2  45583  fprodexp  45592  fprodabs2  45593  climmulf  45602  climexp  45603  climrecf  45607  climinff  45609  climaddf  45613  mullimc  45614  limcperiod  45626  sumnnodd  45628  neglimc  45645  addlimc  45646  climsubmpt  45658  climreclf  45662  climeldmeqmpt  45666  climfveqmpt  45669  fnlimfvre  45672  climfveqf  45678  climfveqmpt3  45680  climeldmeqf  45681  climeqf  45686  climeldmeqmpt3  45687  climinf2  45705  limsupequz  45721  limsupequzmptf  45729  lmbr3  45745  cnrefiisp  45828  cncfshift  45872  fprodcncf  45898  dvmptmulf  45935  dvmptfprod  45943  dvnprodlem1  45944  dvnprodlem3  45946  stoweidlem16  46014  stoweidlem34  46032  stoweidlem62  46060  dirkercncflem2  46102  fourierdlem12  46117  fourierdlem15  46120  fourierdlem34  46139  fourierdlem50  46154  fourierdlem73  46177  fourierdlem94  46198  fourierdlem112  46216  fourierdlem113  46217  intsaluni  46327  sge0lempt  46408  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0ltfirpmpt2  46424  sge0isummpt2  46430  sge0xaddlem2  46432  sge0xadd  46433  meadjiun  46464  voliunsge0lem  46470  meaiuninclem  46478  meaiunincf  46481  meaiuninc3v  46482  meaiuninc3  46483  meaiininclem  46484  meaiininc  46485  isomennd  46529  ovn0lem  46563  sge0hsphoire  46587  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem5  46597  hspmbllem2  46625  hoimbl2  46663  vonhoire  46670  vonioo  46680  vonicc  46683  vonn0ioo2  46688  vonn0icc2  46690  pimincfltioc  46714  salpreimagtlt  46728  smflimlem4  46772  ormkglobd  46873  sinnpoly  46892  rexrsb  47101  ichexmpl2  47471  ichnreuop  47473  sbgoldbm  47785  bgoldbnnsum3prm  47805  tgoldbach  47818  srhmsubcALTV  48313  cbvmpox2  48324  mo0sn  48804  f1omoOLD  48882  isthincd2lem1  49414  thincmo  49417  euendfunc  49515