Theorem eleq1w 2846

Description: Weaker version of eleq1 2851 (but more general than elequ1 2150) not depending on ax-ext 2735 nor df-cleq 2755.

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∃wex 1809   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838

This theorem is referenced by:  clelsb1  2890  cleqh  2892  nfcjust  2911  nfcr  2915  cleqf  2953  rspw  3242  cbvralvw  3243  cbvrexvw  3244  cbvralfw  3305  cbvralsvw  3316  cbvralf  3349  ralcom2  3366  moel  3389  cbvrmovw  3390  cbvreuvw  3391  cbvrmow  3394  cbvreu  3408  cbvrabv  3426  rabrabi  3435  cbvrabw  3451  nfrab  3453  cbvrab  3454  elrab2w  3655  reu2  3688  reu6  3689  rmo4  3693  reu8  3696  2reu5  3721  csbied  3889  difjust  3907  unjust  3909  injust  3911  dfss2  3923  dfssf  3928  dfdif3OLD  4073  eqeuel  4320  rabeq0w  4344  disj  4410  reldisj  4413  ralidmw  4477  dfif6  4490  rabsnifsb  4688  eluniab  4886  unissb  4906  uniintsn  4950  dfiun2g  4994  dfiunv2  4998  disjxun  5107  cbvmptf  5211  cbvmptfg  5212  cbvmptv  5215  dftr2c  5221  isso2i  5606  dfres2  6043  imai  6076  frpoinsg  6344  tz7.7  6386  fvn0ssdmfun  7069  fmptco  7125  cbvriotaw  7376  cbvriotavw  7377  cbvriota  7380  cbvmpox  7503  cbvmpov  7505  tfis  7847  tfindes  7855  peano5  7886  findes  7893  dfoprab4f  8049  fmpox  8060  xpord2indlem  8139  poseq  8150  soseq  8151  smogt  8350  resixpfo  8930  ixpsnf1o  8932  dom2lem  8985  mapsnend  9029  pw2f1olem  9065  pssnn  9149  ssfi  9153  findcard3  9239  ordiso2  9473  elirrvOLDOLD  9557  cantnflem1d  9653  cantnf  9658  setind  9712  frinsg  9719  tz9.12lem3  9757  scottabf  9862  infxpen  9994  dfac5lem4  10106  dfac12lem2  10124  kmlem14  10143  cfsmolem  10249  sornom  10256  isf32lem9  10340  axdc2  10428  fpwwe2lem7  10617  fpwwe2  10623  wunex2  10718  dedekindle  11369  wloglei  11741  uzind4s  12927  seqof2  14092  reuccatpfxs1  14780  shftfn  15106  rexuz3  15396  zsum  15765  fsum  15767  sumss  15771  sumss2  15773  fsumcvg2  15774  fsumser  15777  fsumclf  15785  fsumsplitf  15789  isumless  15895  prodfdiv  15946  cbvprod  15963  cbvprodv  15964  zprod  15987  fprod  15991  fprodntriv  15992  prodss  15997  fprod2dlem  16030  fproddivf  16037  fprodsplitf  16038  rpnnen2lem10  16274  cpnnen  16280  sumeven  16440  sumodd  16441  sadcp1  16508  smupp1  16533  pcmptdvds  16949  prmreclem2  16972  prmreclem5  16975  prmreclem6  16976  prmrec  16977  prmdvdsprmo  17097  iscatd2  17732  initoeu2  18068  yoniso  18336  sgrpidmnd  18792  mndind  18882  eqg0subg  19262  symggen  19535  dprd2d2  20111  srhmsubc  20779  isdrngrd  20869  isdrngrdOLD  20871  lbspss  21203  frlmphl  21931  frlmup1  21948  opsrtoslem1  22206  selvvvval  22293  mdetralt  22765  mdetralt2  22766  mdetunilem2  22770  maducoeval2  22797  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  isclo2  23245  neiptopnei  23289  ptcldmpt  23771  elmptrab  23984  hausflimi  24137  hausflim  24138  alexsubALTlem3  24206  alexsubALTlem4  24207  ptcmplem2  24210  cnextcn  24224  cnextfres1  24225  tgphaus  24274  ustuqtop  24403  utopsnneip  24405  ucncn  24441  nrmmetd  24731  xrhmeo  25105  iscau2  25436  caucfil  25442  cmetcaulem  25447  bcth  25488  vitalilem3  25769  vitali  25772  i1f1lem  25848  itg11  25850  i1fres  25864  mbfi1fseq  25880  mbfi1flim  25882  itg2uba  25902  itg2splitlem  25907  isibl2  25925  cbvitg  25935  cbvitgv  25936  itgss3  25974  dvmptfsum  26134  rolle  26149  elply2  26353  plyexmo  26474  lgamgulmlem2  27194  prmorcht  27342  pclogsum  27379  dchr1  27421  lgsdir  27496  lgsdilem2  27497  lgsdi  27498  lgsne0  27499  lgsquadlem3  27546  lgsquad  27547  2sqlem8  27590  nosupcbv  27866  nosupno  27867  nosupdm  27868  nosupbnd1lem1  27872  noinfcbv  27881  noinfno  27882  noinfdm  27883  nocvxminlem  27947  legval  28853  legov  28854  tglineintmo  28915  tglowdim2ln  28925  ishpg  29041  lnopp2hpgb  29045  hpgerlem  29047  colopp  29051  elplngid  29064  lnincplng  29066  plngcp  29068  plngrot  29072  nhpmirhp  29080  lnperpexs  29114  ragraghl  29149  prlnghpg  29196  prlngmo  29204  tgaltai  29217  axcontlem1  29314  numedglnl  29494  uvtxnbgrvtx  29743  cusgrres  29798  wspniunwspnon  30272  rusgrnumwwlkb0  30323  frgr3vlem2  30625  3vfriswmgrlem  30628  fusgr2wsp2nb  30685  numclwlk2lem2f1o  30730  lpni  30832  pjhthmo  31654  chscllem2  31990  cbvdisjf  32916  2ndresdju  32994  fmptcof2  33002  aciunf1lem  33007  funcnv4mpt  33013  suppovss  33026  fpwrelmapffslem  33077  fsumiunle  33173  gsumwrd2dccatlem  33397  elrspunsn  33737  1arithufdlem3  33836  fedgmullem1  34019  fldextrspunlsp  34064  extdgfialglem2  34083  zarclssn  34263  esumcvg  34476  fiunelros  34564  measiun  34608  bnj1146  35179  bnj1185  35181  bnj1385  35220  bnj1014  35349  bnj1112  35371  bnj1123  35374  bnj1228  35399  bnj1326  35414  bnj1321  35415  bnj1384  35420  bnj1417  35429  bnj1497  35448  trssfir1om  35507  r1omhfb  35508  fineqvnttrclse  35537  axregscl  35541  setindregs  35543  trssfir1omregs  35549  r1omhfbregs  35550  onvf1odlem2  35588  onvf1odlem3  35589  gonarlem  35886  goalrlem  35888  goalr  35889  mrsubrn  36005  dfon2lem6  36278  dfbigcup2  36389  lineintmo  36649  cbvralvw2  36738  cbvrexvw2  36739  cbvrmovw2  36740  cbvreuvw2  36741  cbvmptvw2  36746  cbvprodvw2  36759  cbvrmodavw  36764  cbvreudavw  36765  cbvrabdavw  36773  cbvmptdavw  36779  cbvriotadavw  36782  cbvixpdavw  36790  cbvproddavw  36792  cbvitgdavw  36793  cbvrabdavw2  36797  cbvmptdavw2  36800  cbvriotadavw2  36802  weiunlem  36974  dfttc4  37041  mh-infprim2bi  37058  eleq2w2ALT  37683  bj-idres  37804  mptsnunlem  37984  wl-dfcleq  38160  wl-dfclel  38161  ptrest  38270  poimirlem25  38296  mblfinlem2  38309  mblfinlem3  38310  mblfinlem4  38311  ismblfin  38312  mbfposadd  38318  itg2addnclem  38322  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anclem7  38350  ftc1anc  38352  areacirclem5  38363  fdc1  38397  inxprnres  38947  fsumshftd  39726  pmapglb  40544  polval2N  40680  osumcllem4N  40733  pexmidlem1N  40744  dih1dimatlem  42103  mapdh9a  42563  mapdh9aOLDN  42564  sticksstones2  42914  fsuppind  43322  fphpd  43543  fphpdo  43544  pellex  43562  setindtrs  43752  dford3lem2  43754  fnwe2lem2  43778  mendlmod  43916  cantnfub  44048  tfsconcat0i  44072  rababg  44300  fsovrfovd  44735  fsovcnvlem  44739  trfr  45671  elunif  45736  iunincfi  45812  cbvmpo2  45815  cbvmpo1  45816  disjf1  45901  wessf1ornlem  45903  disjinfi  45910  supxrleubrnmptf  46165  monoordxr  46196  monoord2xr  46198  fsummulc1f  46287  fsumnncl  46288  fsumf1of  46290  fsumiunss  46291  fsumreclf  46292  fsumlessf  46293  fsumsermpt  46295  fmulcl  46297  fmul01lt1lem2  46301  fprodexp  46310  fprodabs2  46311  climmulf  46320  climexp  46321  climrecf  46325  climinff  46327  climaddf  46331  mullimc  46332  limcperiod  46344  sumnnodd  46346  neglimc  46361  addlimc  46362  climsubmpt  46374  climreclf  46378  climeldmeqmpt  46382  climfveqmpt  46385  fnlimfvre  46388  climfveqf  46394  climfveqmpt3  46396  climeldmeqf  46397  climeqf  46402  climeldmeqmpt3  46403  climinf2  46421  limsupequz  46437  limsupequzmptf  46445  lmbr3  46461  cnrefiisp  46544  cncfshift  46588  fprodcncf  46614  dvmptmulf  46651  dvmptfprod  46659  dvnprodlem1  46660  dvnprodlem3  46662  stoweidlem16  46730  stoweidlem34  46748  stoweidlem62  46776  dirkercncflem2  46818  fourierdlem12  46833  fourierdlem15  46836  fourierdlem34  46855  fourierdlem50  46870  fourierdlem73  46893  fourierdlem94  46914  fourierdlem112  46932  fourierdlem113  46933  intsaluni  47043  sge0lempt  47124  sge0iunmptlemfi  47127  sge0iunmptlemre  47129  sge0iunmpt  47132  sge0ltfirpmpt2  47140  sge0isummpt2  47146  sge0xaddlem2  47148  sge0xadd  47149  meadjiun  47180  voliunsge0lem  47186  meaiuninclem  47194  meaiunincf  47197  meaiuninc3v  47198  meaiuninc3  47199  meaiininclem  47200  meaiininc  47201  isomennd  47245  ovn0lem  47279  sge0hsphoire  47303  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvlelem5  47313  hspmbllem2  47341  hoimbl2  47379  vonhoire  47386  vonioo  47396  vonicc  47399  vonn0ioo2  47404  vonn0icc2  47406  pimincfltioc  47430  salpreimagtlt  47444  smflimlem4  47488  ormkglobd  47591  sinnpoly  47628  rexrsb  47837  ichexmpl2  48219  ichnreuop  48221  sbgoldbm  48549  bgoldbnnsum3prm  48569  tgoldbach  48582  srhmsubcALTV  49090  cbvmpox2  49116  mo0sn  49594  f1omoOLD  49672  isthincd2lem1  50203  thincmo  50206  euendfunc  50304