Theorem eleq1w 2844

Description: Weaker version of eleq1 2849 (but more general than elequ1 2152) not depending on ax-ext 2733 nor df-cleq 2753.

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836

This theorem is used by:  clelsb1  2888  cleqh  2890  nfcjust  2909  nfcr  2913  cleqf  2951  rspw  3240  cbvralvw  3241  cbvrexvw  3242  cbvralfw  3303  cbvralsvw  3314  cbvralf  3346  ralcom2  3363  moel  3386  cbvrmovw  3387  cbvreuvw  3388  cbvrmow  3391  cbvreu  3405  cbvrabv  3423  rabrabi  3431  cbvrabw  3447  nfrab  3449  cbvrab  3450  elrab2w  3650  reu2  3683  reu6  3684  rmo4  3688  reu8  3691  2reu5  3716  csbied  3883  difjust  3901  unjust  3903  injust  3905  dfss2  3917  dfssf  3922  eqeuel  4313  rabeq0w  4337  disj  4403  reldisj  4406  ralidmw  4472  dfif6  4485  rabsnifsb  4683  eluniab  4881  unissb  4901  uniintsn  4945  dfiun2g  4988  dfiunv2  4992  disjxun  5101  cbvmptf  5205  cbvmptfg  5206  cbvmptv  5209  dftr2c  5215  isso2i  5596  dfres2  6033  imai  6072  frpoinsg  6346  tz7.7  6388  fvn0ssdmfun  7074  fmptco  7130  cbvriotaw  7386  cbvriotavw  7387  cbvriota  7390  cbvmpox  7513  cbvmpov  7515  tfis  7866  tfindes  7874  peano5  7905  findes  7912  dfoprab4f  8067  fmpox  8078  fnwe2lem3  8147  xpord2indlem  8164  poseq  8175  soseq  8176  smogt  8375  resixpfo  8964  ixpsnf1o  8966  dom2lem  9019  mapsnend  9064  pw2f1olem  9100  pssnn  9184  ssfi  9188  findcard3  9274  ordiso2  9509  elirrvOLDOLD  9593  cantnflem1d  9689  cantnf  9694  setind  9748  frinsg  9755  tz9.12lem3  9796  scottabf  9939  infxpen  10093  dfac5lem4  10205  dfac12lem2  10223  kmlem14  10242  cfsmolem  10348  sornom  10355  isf32lem9  10439  axdc2  10527  fpwwe2lem7  10722  fpwwe2  10728  wunex2  10823  dedekindle  11474  wloglei  11848  uzind4s  13035  seqof2  14203  reuccatpfxs1  14896  shftfn  15226  rexuz3  15516  zsum  15884  fsum  15886  sumss  15890  sumss2  15892  fsumcvg2  15893  fsumser  15896  fsumclf  15904  fsumsplitf  15908  isumless  16014  prodfdiv  16065  cbvprod  16082  cbvprodv  16083  zprod  16104  fprod  16108  fprodntriv  16109  prodss  16114  fprod2dlem  16147  fproddivf  16154  fprodsplitf  16155  rpnnen2lem10  16391  cpnnen  16397  sumeven  16557  sumodd  16558  sadcp1  16625  smupp1  16650  pcmptdvds  17072  prmreclem2  17095  prmreclem5  17098  prmreclem6  17099  prmrec  17100  prmdvdsprmo  17220  iscatd2  17855  initoeu2  18191  yoniso  18459  sgrpidmnd  18928  mndind  19024  eqg0subg  19411  symggen  19684  dprd2d2  20260  srhmsubc  20932  isdrngrd  21023  isdrngrdOLD  21025  lbspss  21357  frlmphl  22087  frlmup1  22104  opsrtoslem1  22364  selvvvval  22451  mdetralt  22923  mdetralt2  22924  mdetunilem2  22928  maducoeval2  22955  chfacfscmulgsum  23178  chfacfpmmulgsum  23182  isclo2  23406  neiptopnei  23450  ptcldmpt  23933  elmptrab  24146  hausflimi  24299  hausflim  24300  alexsubALTlem3  24368  alexsubALTlem4  24369  ptcmplem2  24372  cnextcn  24386  cnextfres1  24387  tgphaus  24436  ustuqtop  24565  utopsnneip  24567  ucncn  24603  nrmmetd  24893  xrhmeo  25267  iscau2  25598  caucfil  25604  cmetcaulem  25609  bcth  25650  vitalilem3  25931  vitali  25934  i1f1lem  26010  itg11  26012  i1fres  26026  mbfi1fseq  26042  mbfi1flim  26044  itg2uba  26064  itg2splitlem  26069  isibl2  26087  cbvitg  26096  cbvitgv  26097  itgss3  26135  dvmptfsum  26295  rolle  26310  elply2  26514  plyexmo  26636  lgamgulmlem2  27357  prmorcht  27505  pclogsum  27542  dchr1  27584  lgsdir  27659  lgsdilem2  27660  lgsdi  27661  lgsne0  27662  lgsquadlem3  27709  lgsquad  27710  2sqlem8  27753  nosupcbv  28059  nosupno  28060  nosupdm  28061  nosupbnd1lem1  28065  noinfcbv  28074  noinfno  28075  noinfdm  28076  nocvxminlem  28140  legval  29047  legov  29048  tglineintmo  29110  tglowdim2ln  29120  ishpg  29237  lnopp2hpgb  29241  hpgerlem  29243  colopp  29247  elplngid  29260  lnincplng  29262  plngcp  29264  plngrot  29268  nhpmirhp  29276  lnperpexs  29310  ragraghl  29346  tgaaddcpbllem2  29350  tgaaddcpbllem3  29351  prlnghpg  29424  prlngmo  29432  tgaltai  29445  axcontlem1  29542  numedglnl  29722  uvtxnbgrvtx  29974  cusgrres  30029  wspniunwspnon  30512  rusgrnumwwlkb0  30563  frgr3vlem2  30875  3vfriswmgrlem  30878  fusgr2wsp2nb  30935  numclwlk2lem2f1o  30980  lpni  31082  pjhthmo  31904  chscllem2  32240  cbvdisjf  33165  2ndresdju  33243  fmptcof2  33251  aciunf1lem  33256  funcnv4mpt  33262  suppovss  33274  fpwrelmapffslem  33324  fsumiunle  33420  gsumwrd2dccatlem  33638  elrspunsn  33979  1arithufdlem3  34078  fedgmullem1  34261  fldextrspunlsp  34306  extdgfialglem2  34325  zarclssn  34505  esumcvg  34718  fiunelros  34807  measiun  34851  bnj1146  35421  bnj1185  35423  bnj1385  35462  bnj1014  35591  bnj1112  35613  bnj1123  35616  bnj1228  35641  bnj1326  35656  bnj1321  35657  bnj1384  35662  bnj1417  35671  bnj1497  35690  trssfir1om  35737  r1omhfb  35738  fineqvnttrclse  35792  axregscl  35796  setindregs  35798  trssfir1omregs  35804  r1omhfbregs  35805  onvf1odlem2  35883  onvf1odlem3  35884  gonarlem  36159  goalrlem  36161  goalr  36162  mrsubrn  36278  dfon2lem6  36550  dfbigcup2  36661  lineintmo  36922  cbvralvw2  37015  cbvrexvw2  37016  cbvrmovw2  37017  cbvreuvw2  37018  cbvmptvw2  37023  cbvprodvw2  37036  cbvrmodavw  37041  cbvreudavw  37042  cbvrabdavw  37050  cbvmptdavw  37056  cbvriotadavw  37059  cbvixpdavw  37067  cbvproddavw  37069  cbvitgdavw  37070  cbvrabdavw2  37074  cbvmptdavw2  37077  cbvriotadavw2  37079  weiunlem  37251  dfttc4  37318  mh-infprim2bi  37335  eleq2w2ALT  37962  bj-idres  38081  mptsnunlem  38261  wl-dfcleq  38437  wl-dfclel  38438  ptrest  38537  poimirlem25  38563  mblfinlem2  38576  mblfinlem3  38577  mblfinlem4  38578  ismblfin  38579  mbfposadd  38585  itg2addnclem  38589  ftc1anclem5  38615  ftc1anclem6  38616  ftc1anclem7  38617  ftc1anc  38619  areacirclem5  38630  fdc1  38680  inxprnres  39230  fsumshftd  40009  pmapglb  40827  polval2N  40963  osumcllem4N  41016  pexmidlem1N  41027  dih1dimatlem  42386  mapdh9a  42846  mapdh9aOLDN  42847  sticksstones2  43197  fsuppind  43618  fphpd  43822  fphpdo  43823  pellex  43841  setindtrs  44031  dford3lem2  44033  mendlmod  44190  cantnfub  44322  tfsconcat0i  44346  rababg  44574  fsovrfovd  45008  fsovcnvlem  45012  trfr  45951  elunif  46032  iunincfi  46108  cbvmpo2  46111  cbvmpo1  46112  disjf1  46197  wessf1ornlem  46199  disjinfi  46206  supxrleubrnmptf  46460  monoordxr  46491  monoord2xr  46493  fsummulc1f  46582  fsumnncl  46583  fsumf1of  46585  fsumiunss  46586  fsumreclf  46587  fsumlessf  46588  fsumsermpt  46590  fmulcl  46592  fmul01lt1lem2  46596  fprodexp  46605  fprodabs2  46606  climmulf  46615  climexp  46616  climrecf  46620  climinff  46622  climaddf  46626  mullimc  46627  limcperiod  46639  sumnnodd  46641  neglimc  46656  addlimc  46657  climsubmpt  46669  climreclf  46673  climeldmeqmpt  46677  climfveqmpt  46680  fnlimfvre  46683  climfveqf  46689  climfveqmpt3  46691  climeldmeqf  46692  climeqf  46697  climeldmeqmpt3  46698  climinf2  46716  limsupequz  46732  limsupequzmptf  46740  lmbr3  46756  cnrefiisp  46839  cncfshift  46883  fprodcncf  46909  dvmptmulf  46946  dvmptfprod  46954  dvnprodlem1  46955  dvnprodlem3  46957  stoweidlem16  47025  stoweidlem34  47043  stoweidlem62  47071  dirkercncflem2  47113  fourierdlem12  47128  fourierdlem15  47131  fourierdlem34  47150  fourierdlem50  47165  fourierdlem73  47188  fourierdlem94  47209  fourierdlem112  47227  fourierdlem113  47228  intsaluni  47338  sge0lempt  47419  sge0iunmptlemfi  47422  sge0iunmptlemre  47424  sge0iunmpt  47427  sge0ltfirpmpt2  47435  sge0isummpt2  47441  sge0xaddlem2  47443  sge0xadd  47444  meadjiun  47475  voliunsge0lem  47481  meaiuninclem  47489  meaiunincf  47492  meaiuninc3v  47493  meaiuninc3  47494  meaiininclem  47495  meaiininc  47496  isomennd  47540  ovn0lem  47574  sge0hsphoire  47598  hoidmvlelem1  47604  hoidmvlelem2  47605  hoidmvlelem3  47606  hoidmvlelem5  47608  hspmbllem2  47636  hoimbl2  47674  vonhoire  47681  vonioo  47691  vonicc  47694  vonn0ioo2  47699  vonn0icc2  47701  pimincfltioc  47725  salpreimagtlt  47739  smflimlem4  47783  ormkglobd  47886  sinnpoly  47940  rexrsb  48169  ichexmpl2  48551  ichnreuop  48553  sbgoldbm  48881  bgoldbnnsum3prm  48901  tgoldbach  48914  srhmsubcALTV  49421  cbvmpox2  49447  mo0sn  49925  f1omoOLD  50001  isthincd2lem1  50532  thincmo  50535  euendfunc  50633