Theorem eleq1w 2814

Description: Weaker version of eleq1 2819 (but more general than elequ1 2118) not depending on ax-ext 2703 nor df-cleq 2723.

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806

This theorem is referenced by:  clelsb1  2858  cleqh  2860  nfcjust  2880  nfcr  2884  cleqf  2923  rspw  3209  cbvralvw  3210  cbvrexvw  3211  cbvralfw  3272  cbvralsvw  3283  cbvralf  3326  ralcom2  3343  moel  3366  cbvrmovw  3367  cbvreuvw  3368  cbvrmow  3371  cbvreu  3387  cbvrabv  3405  rabrabi  3414  cbvrabw  3430  cbvrabwOLD  3431  nfrab  3434  cbvrab  3435  elrab2w  3646  reu2  3679  reu6  3680  rmo4  3684  reu8  3687  2reu5  3712  ruOLD  3735  csbied  3881  difjust  3899  unjust  3901  injust  3903  dfss2  3915  dfssf  3920  dfdif3OLD  4065  eqeuel  4312  rabeq0w  4334  disj  4397  reldisj  4400  ralidmw  4455  dfif6  4475  rabsnifsb  4672  eluniab  4870  unissb  4889  uniintsn  4933  dfiun2g  4978  dfiunv2  4982  disjxun  5087  cbvmptf  5189  cbvmptfg  5190  cbvmptv  5193  dftr2c  5199  isso2i  5559  dfres2  5989  imai  6022  frpoinsg  6290  tz7.7  6332  fvn0ssdmfun  7007  fmptco  7062  cbvriotaw  7312  cbvriotavw  7313  cbvriota  7316  cbvmpox  7439  cbvmpov  7441  tfis  7785  tfindes  7793  peano5  7823  findes  7830  dfoprab4f  7988  fmpox  7999  xpord2indlem  8077  poseq  8088  soseq  8089  smogt  8287  resixpfo  8860  ixpsnf1o  8862  dom2lem  8914  mapsnend  8958  pw2f1olem  8994  pssnn  9078  ssfi  9082  findcard3  9167  ordiso2  9401  elirrvOLD  9484  cantnflem1d  9578  cantnf  9583  setind  9637  frinsg  9644  tz9.12lem3  9682  infxpen  9905  dfac5lem4  10017  dfac12lem2  10036  kmlem14  10055  cfsmolem  10161  sornom  10168  isf32lem9  10252  axdc2  10340  fpwwe2lem7  10528  fpwwe2  10534  wunex2  10629  dedekindle  11277  wloglei  11649  uzind4s  12806  seqof2  13967  reuccatpfxs1  14654  shftfn  14980  rexuz3  15256  zsum  15625  fsum  15627  sumss  15631  sumss2  15633  fsumcvg2  15634  fsumser  15637  fsumclf  15645  fsumsplitf  15649  isumless  15752  prodfdiv  15803  cbvprod  15820  cbvprodv  15821  zprod  15844  fprod  15848  fprodntriv  15849  prodss  15854  fprod2dlem  15887  fproddivf  15894  fprodsplitf  15895  rpnnen2lem10  16132  cpnnen  16138  sumeven  16298  sumodd  16299  sadcp1  16366  smupp1  16391  pcmptdvds  16806  prmreclem2  16829  prmreclem5  16832  prmreclem6  16833  prmrec  16834  prmdvdsprmo  16954  iscatd2  17587  initoeu2  17923  yoniso  18191  sgrpidmnd  18647  mndind  18736  eqg0subg  19108  symggen  19382  dprd2d2  19958  srhmsubc  20595  isdrngrd  20681  isdrngrdOLD  20683  lbspss  21016  frlmphl  21718  frlmup1  21735  opsrtoslem1  21990  mdetralt  22523  mdetralt2  22524  mdetunilem2  22528  maducoeval2  22555  chfacfscmulgsum  22775  chfacfpmmulgsum  22779  isclo2  23003  neiptopnei  23047  ptcldmpt  23529  elmptrab  23742  hausflimi  23895  hausflim  23896  alexsubALTlem3  23964  alexsubALTlem4  23965  ptcmplem2  23968  cnextcn  23982  cnextfres1  23983  tgphaus  24032  ustuqtop  24161  utopsnneip  24163  ucncn  24199  nrmmetd  24489  xrhmeo  24871  iscau2  25204  caucfil  25210  cmetcaulem  25215  bcth  25256  vitalilem3  25538  vitali  25541  i1f1lem  25617  itg11  25619  i1fres  25633  mbfi1fseq  25649  mbfi1flim  25651  itg2uba  25671  itg2splitlem  25676  isibl2  25694  cbvitg  25704  cbvitgv  25705  itgss3  25743  dvmptfsum  25906  rolle  25921  elply2  26128  plyexmo  26248  lgamgulmlem2  26967  prmorcht  27115  pclogsum  27153  dchr1  27195  lgsdir  27270  lgsdilem2  27271  lgsdi  27272  lgsne0  27273  lgsquadlem3  27320  lgsquad  27321  2sqlem8  27364  nosupcbv  27641  nosupno  27642  nosupdm  27643  nosupbnd1lem1  27647  noinfcbv  27656  noinfno  27657  noinfdm  27658  nocvxminlem  27717  legval  28562  legov  28563  tglineintmo  28620  tglowdim2ln  28629  ishpg  28737  lnopp2hpgb  28741  hpgerlem  28743  colopp  28747  axcontlem1  28942  numedglnl  29122  uvtxnbgrvtx  29371  cusgrres  29427  wspniunwspnon  29901  rusgrnumwwlkb0  29952  frgr3vlem2  30254  3vfriswmgrlem  30257  fusgr2wsp2nb  30314  numclwlk2lem2f1o  30359  lpni  30460  pjhthmo  31282  chscllem2  31618  cbvdisjf  32551  2ndresdju  32631  fmptcof2  32639  aciunf1lem  32644  funcnv4mpt  32651  suppovss  32662  fpwrelmapffslem  32715  fsumiunle  32812  gsumwrd2dccatlem  33046  elrspunsn  33394  1arithufdlem3  33511  fedgmullem1  33642  fldextrspunlsp  33687  extdgfialglem2  33706  zarclssn  33886  esumcvg  34099  fiunelros  34187  measiun  34231  bnj1146  34803  bnj1185  34805  bnj1385  34844  bnj1014  34973  bnj1112  34995  bnj1123  34998  bnj1228  35023  bnj1326  35038  bnj1321  35039  bnj1384  35044  bnj1417  35053  bnj1497  35072  trssfir1om  35122  r1omhfb  35123  axregscl  35126  setindregs  35128  trssfir1omregs  35132  r1omhfbregs  35133  fineqvnttrclse  35144  onvf1odlem2  35148  onvf1odlem3  35149  gonarlem  35438  goalrlem  35440  goalr  35441  mrsubrn  35557  dfon2lem6  35830  dfbigcup2  35941  lineintmo  36199  cbvralvw2  36268  cbvrexvw2  36269  cbvrmovw2  36270  cbvreuvw2  36271  cbvmptvw2  36276  cbvprodvw2  36289  cbvrmodavw  36294  cbvreudavw  36295  cbvrabdavw  36303  cbvmptdavw  36309  cbvriotadavw  36312  cbvixpdavw  36320  cbvproddavw  36322  cbvitgdavw  36323  cbvrabdavw2  36327  cbvmptdavw2  36330  cbvriotadavw2  36332  weiunlem2  36505  eleq2w2ALT  37089  bj-idres  37202  mptsnunlem  37380  ptrest  37667  poimirlem25  37693  mblfinlem2  37706  mblfinlem3  37707  mblfinlem4  37708  ismblfin  37709  mbfposadd  37715  itg2addnclem  37719  ftc1anclem5  37745  ftc1anclem6  37746  ftc1anclem7  37747  ftc1anc  37749  areacirclem5  37760  fdc1  37794  inxprnres  38334  fsumshftd  38999  pmapglb  39817  polval2N  39953  osumcllem4N  40006  pexmidlem1N  40017  dih1dimatlem  41376  mapdh9a  41836  mapdh9aOLDN  41837  sticksstones2  42188  selvvvval  42626  fsuppind  42631  fphpd  42857  fphpdo  42858  pellex  42876  setindtrs  43066  dford3lem2  43068  fnwe2lem2  43092  mendlmod  43230  cantnfub  43362  tfsconcat0i  43386  rababg  43615  fsovrfovd  44050  fsovcnvlem  44054  scottabf  44281  trfr  45003  elunif  45061  iunincfi  45139  cbvmpo2  45142  cbvmpo1  45143  disjf1  45228  wessf1ornlem  45230  disjinfi  45237  supxrleubrnmptf  45497  monoordxr  45528  monoord2xr  45530  fsummulc1f  45619  fsumnncl  45620  fsumf1of  45622  fsumiunss  45623  fsumreclf  45624  fsumlessf  45625  fsumsermpt  45627  fmulcl  45629  fmul01lt1lem2  45633  fprodexp  45642  fprodabs2  45643  climmulf  45652  climexp  45653  climrecf  45657  climinff  45659  climaddf  45663  mullimc  45664  limcperiod  45676  sumnnodd  45678  neglimc  45693  addlimc  45694  climsubmpt  45706  climreclf  45710  climeldmeqmpt  45714  climfveqmpt  45717  fnlimfvre  45720  climfveqf  45726  climfveqmpt3  45728  climeldmeqf  45729  climeqf  45734  climeldmeqmpt3  45735  climinf2  45753  limsupequz  45769  limsupequzmptf  45777  lmbr3  45793  cnrefiisp  45876  cncfshift  45920  fprodcncf  45946  dvmptmulf  45983  dvmptfprod  45991  dvnprodlem1  45992  dvnprodlem3  45994  stoweidlem16  46062  stoweidlem34  46080  stoweidlem62  46108  dirkercncflem2  46150  fourierdlem12  46165  fourierdlem15  46168  fourierdlem34  46187  fourierdlem50  46202  fourierdlem73  46225  fourierdlem94  46246  fourierdlem112  46264  fourierdlem113  46265  intsaluni  46375  sge0lempt  46456  sge0iunmptlemfi  46459  sge0iunmptlemre  46461  sge0iunmpt  46464  sge0ltfirpmpt2  46472  sge0isummpt2  46478  sge0xaddlem2  46480  sge0xadd  46481  meadjiun  46512  voliunsge0lem  46518  meaiuninclem  46526  meaiunincf  46529  meaiuninc3v  46530  meaiuninc3  46531  meaiininclem  46532  meaiininc  46533  isomennd  46577  ovn0lem  46611  sge0hsphoire  46635  hoidmvlelem1  46641  hoidmvlelem2  46642  hoidmvlelem3  46643  hoidmvlelem5  46645  hspmbllem2  46673  hoimbl2  46711  vonhoire  46718  vonioo  46728  vonicc  46731  vonn0ioo2  46736  vonn0icc2  46738  pimincfltioc  46762  salpreimagtlt  46776  smflimlem4  46820  ormkglobd  46921  sinnpoly  46930  rexrsb  47139  ichexmpl2  47509  ichnreuop  47511  sbgoldbm  47823  bgoldbnnsum3prm  47843  tgoldbach  47856  srhmsubcALTV  48364  cbvmpox2  48375  mo0sn  48855  f1omoOLD  48933  isthincd2lem1  49465  thincmo  49468  euendfunc  49566