Theorem eleq1w 2821

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

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃wex 1782   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2816

This theorem is referenced by:  cleqh  2862  clelsb1  2866  nfcjust  2888  nfcr  2892  nfcriOLD  2897  nfcriOLDOLD  2898  cleqf  2938  rspw  3129  ralcom2  3288  nfrab  3318  moel  3356  moelOLD  3357  cbvralfw  3366  cbvralfwOLD  3367  cbvralf  3369  cbvreuw  3373  cbvrmow  3374  cbvreu  3378  cbvralvw  3380  cbvrexvw  3381  cbvrmovw  3382  cbvreuvw  3383  cbvrabw  3421  cbvrab  3422  cbvrabv  3423  rabrabi  3424  reu2  3659  reu6  3660  rmo4  3664  reu8  3667  2reu5  3692  ru  3714  csbied  3869  difjust  3888  unjust  3890  injust  3892  dfss2f  3910  dfdif3  4048  eqeuel  4296  rabeq0w  4317  disj  4381  reldisj  4385  ralidmw  4438  dfif6  4462  rabsnifsb  4658  eluniab  4854  elintab  4890  uniintsn  4918  dfiunv2  4964  disjxun  5071  cbvmptf  5182  cbvmptfg  5183  cbvmptv  5186  isso2i  5533  dfres2  5942  imai  5975  frpoinsg  6239  wfisgOLD  6250  tz7.7  6285  fvn0ssdmfun  6944  fmptco  6993  cbvriotaw  7233  cbvriotavw  7234  cbvriota  7238  cbvmpox  7358  tfis  7691  tfindes  7699  peano5  7730  findes  7739  dfoprab4f  7885  fmpox  7896  wfrlem10OLD  8136  smogt  8185  resixpfo  8711  ixpsnf1o  8713  dom2lem  8767  mapsnend  8813  pw2f1olem  8850  pssnn  8938  ssfi  8943  findcard3  9044  ordiso2  9261  elirrv  9342  cantnflem1d  9433  cantnf  9438  setind  9501  frinsg  9519  tz9.12lem3  9557  infxpen  9780  dfac12lem2  9910  kmlem14  9929  cfsmolem  10036  sornom  10043  isf32lem9  10127  axdc2  10215  fpwwe2lem7  10403  fpwwe2  10409  wunex2  10504  dedekindle  11149  wloglei  11517  uzind4s  12658  seqof2  13791  reuccatpfxs1  14470  shftfn  14794  rexuz3  15070  zsum  15440  fsum  15442  sumss  15446  sumss2  15448  fsumcvg2  15449  fsumser  15452  fsumclf  15460  fsumsplitf  15464  isumless  15567  prodfdiv  15618  cbvprod  15635  zprod  15657  fprod  15661  fprodntriv  15662  prodss  15667  fprod2dlem  15700  fproddivf  15707  fprodsplitf  15708  rpnnen2lem10  15942  cpnnen  15948  sumeven  16106  sumodd  16107  sadcp1  16172  smupp1  16197  pcmptdvds  16605  prmreclem2  16628  prmreclem5  16631  prmreclem6  16632  prmrec  16633  prmdvdsprmo  16753  iscatd2  17400  initoeu2  17741  yoniso  18013  sgrpidmnd  18400  mndind  18476  symggen  19088  dprd2d2  19657  isdrngrd  20027  lbspss  20354  frlmphl  20998  frlmup1  21015  opsrtoslem1  21272  mdetralt  21767  mdetralt2  21768  mdetunilem2  21772  maducoeval2  21799  chfacfscmulgsum  22019  chfacfpmmulgsum  22023  isclo2  22249  neiptopnei  22293  ptcldmpt  22775  elmptrab  22988  hausflimi  23141  hausflim  23142  alexsubALTlem3  23210  alexsubALTlem4  23211  ptcmplem2  23214  cnextcn  23228  cnextfres1  23229  tgphaus  23278  ustuqtop  23408  utopsnneip  23410  ucncn  23447  nrmmetd  23740  xrhmeo  24119  iscau2  24451  caucfil  24457  cmetcaulem  24462  bcth  24503  vitalilem3  24784  vitali  24787  i1f1lem  24863  itg11  24865  i1fres  24880  mbfi1fseq  24896  mbfi1flim  24898  itg2uba  24918  itg2splitlem  24923  isibl2  24941  cbvitg  24950  itgss3  24989  dvmptfsum  25149  rolle  25164  elply2  25367  plyexmo  25483  lgamgulmlem2  26189  prmorcht  26337  pclogsum  26373  dchr1  26415  lgsdir  26490  lgsdilem2  26491  lgsdi  26492  lgsne0  26493  lgsquadlem3  26540  lgsquad  26541  2sqlem8  26584  legval  26955  legov  26956  tglineintmo  27013  tglowdim2ln  27022  ishpg  27130  lnopp2hpgb  27134  hpgerlem  27136  colopp  27140  axcontlem1  27342  numedglnl  27524  uvtxnbgrvtx  27770  cusgrres  27825  wspniunwspnon  28296  rusgrnumwwlkb0  28344  frgr3vlem2  28646  3vfriswmgrlem  28649  fusgr2wsp2nb  28706  numclwlk2lem2f1o  28751  lpni  28850  pjhthmo  29672  chscllem2  30008  cbvdisjf  30918  2ndresdju  30994  fmptcof2  31002  aciunf1lem  31007  funcnv4mpt  31014  suppovss  31025  fpwrelmapffslem  31075  fsumiunle  31151  fedgmullem1  31718  zarclssn  31831  esumcvg  32062  fiunelros  32150  measiun  32194  bnj1146  32779  bnj1185  32781  bnj1385  32820  bnj1014  32949  bnj1112  32971  bnj1123  32974  bnj1228  32999  bnj1326  33014  bnj1321  33015  bnj1384  33020  bnj1417  33029  bnj1497  33048  gonarlem  33364  goalrlem  33366  goalr  33367  mrsubrn  33483  dfon2lem6  33772  xpord2ind  33802  xpord3ind  33808  poseq  33810  soseq  33811  nosupcbv  33913  nosupno  33914  nosupdm  33915  nosupbnd1lem1  33919  noinfcbv  33928  noinfno  33929  noinfdm  33930  nocvxminlem  33980  dfbigcup2  34209  lineintmo  34467  eleq2w2ALT  35228  bj-idres  35339  mptsnunlem  35517  ptrest  35784  poimirlem25  35810  mblfinlem2  35823  mblfinlem3  35824  mblfinlem4  35825  ismblfin  35826  mbfposadd  35832  itg2addnclem  35836  ftc1anclem5  35862  ftc1anclem6  35863  ftc1anclem7  35864  ftc1anc  35866  areacirclem5  35877  fdc1  35912  inxprnres  36435  fsumshftd  36974  pmapglb  37792  polval2N  37928  osumcllem4N  37981  pexmidlem1N  37992  dih1dimatlem  39351  mapdh9a  39811  mapdh9aOLDN  39812  sticksstones2  40111  elrab2w  40175  fsuppind  40287  fphpd  40646  fphpdo  40647  pellex  40665  setindtrs  40855  dford3lem2  40857  fnwe2lem2  40884  mendlmod  41026  rababg  41162  fsovrfovd  41598  fsovcnvlem  41602  scottabf  41839  elunif  42540  iunincfi  42625  cbvmpo2  42628  cbvmpo1  42629  disjf1  42701  wessf1ornlem  42703  disjinfi  42712  supxrleubrnmptf  42972  monoordxr  43004  monoord2xr  43006  fsummulc1f  43093  fsumnncl  43094  fsumf1of  43096  fsumiunss  43097  fsumreclf  43098  fsumlessf  43099  fsumsermpt  43101  fmulcl  43103  fmul01lt1lem2  43107  fprodexp  43116  fprodabs2  43117  climmulf  43126  climexp  43127  climrecf  43131  climinff  43133  climaddf  43137  mullimc  43138  limcperiod  43150  sumnnodd  43152  neglimc  43169  addlimc  43170  climsubmpt  43182  climreclf  43186  climeldmeqmpt  43190  climfveqmpt  43193  fnlimfvre  43196  climfveqf  43202  climfveqmpt3  43204  climeldmeqf  43205  climeqf  43210  climeldmeqmpt3  43211  climinf2  43229  limsupequz  43245  limsupequzmptf  43253  lmbr3  43269  cnrefiisp  43352  cncfshift  43396  fprodcncf  43422  dvmptmulf  43459  dvmptfprod  43467  dvnprodlem1  43468  dvnprodlem3  43470  stoweidlem16  43538  stoweidlem34  43556  stoweidlem62  43584  dirkercncflem2  43626  fourierdlem12  43641  fourierdlem15  43644  fourierdlem34  43663  fourierdlem50  43678  fourierdlem73  43701  fourierdlem94  43722  fourierdlem112  43740  fourierdlem113  43741  intsaluni  43849  sge0lempt  43929  sge0iunmptlemfi  43932  sge0iunmptlemre  43934  sge0iunmpt  43937  sge0ltfirpmpt2  43945  sge0isummpt2  43951  sge0xaddlem2  43953  sge0xadd  43954  meadjiun  43985  voliunsge0lem  43991  meaiuninclem  43999  meaiunincf  44002  meaiuninc3v  44003  meaiuninc3  44004  meaiininclem  44005  meaiininc  44006  isomennd  44050  ovn0lem  44084  sge0hsphoire  44108  hoidmvlelem1  44114  hoidmvlelem2  44115  hoidmvlelem3  44116  hoidmvlelem5  44118  hspmbllem2  44146  hoimbl2  44184  vonhoire  44191  vonioo  44201  vonicc  44204  vonn0ioo2  44209  vonn0icc2  44211  pimincfltioc  44231  salpreimagtlt  44244  smflimlem4  44287  rexrsb  44570  ichexmpl2  44900  ichnreuop  44902  sbgoldbm  45214  bgoldbnnsum3prm  45234  tgoldbach  45247  srhmsubc  45612  srhmsubcALTV  45630  cbvmpox2  45649  mo0sn  46139  f1omo  46166  isthincd2lem1  46286  thincmo  46288