Theorem eleq1w 2847

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

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  clelsb1  2891  cleqh  2893  nfcjust  2912  nfcr  2916  cleqf  2954  rspw  3243  cbvralvw  3244  cbvrexvw  3245  cbvralfw  3306  cbvralsvw  3317  cbvralf  3349  ralcom2  3366  moel  3389  cbvrmovw  3390  cbvreuvw  3391  cbvrmow  3394  cbvreu  3408  cbvrabv  3426  rabrabi  3434  cbvrabw  3450  nfrab  3452  cbvrab  3453  elrab2w  3653  reu2  3686  reu6  3687  rmo4  3691  reu8  3694  2reu5  3719  csbied  3887  dfssf  3904  difjust  4049  injust  4093  dfss2  4097  unjust  4153  eqeuel  4316  rabeq0w  4340  disj  4406  reldisj  4409  ralidmw  4475  dfif6  4488  rabsnifsb  4685  eluniab  4886  unissb  4906  uniintsn  4950  dfiun2g  4993  dfiunv2  4997  disjxun  5106  cbvmptf  5211  cbvmptfg  5212  cbvmptv  5215  dftr2c  5221  isso2i  5603  dfres2  6051  imai  6090  frpoinsg  6372  tz7.7  6414  fvn0ssdmfun  7106  fmptco  7162  cbvriotaw  7417  cbvriotavw  7418  cbvriota  7421  cbvmpox  7544  cbvmpov  7546  tfis  7900  tfindes  7908  peano5  7939  findes  7946  dfoprab4f  8102  fmpox  8113  fnwe2lem3  8184  xpord2indlem  8201  poseq  8212  soseq  8213  smogt  8413  resixpfo  9002  ixpsnf1o  9004  dom2lem  9057  mapsnend  9102  pw2f1olem  9138  pssnn  9222  ssfi  9226  findcard3  9312  ordiso2  9546  elirrvOLDOLD  9630  cantnflem1d  9726  cantnf  9731  setind  9785  frinsg  9792  tz9.12lem3  9833  scottabf  9976  infxpen  10132  dfac5lem4  10244  dfac12lem2  10262  kmlem14  10281  cfsmolem  10387  sornom  10394  isf32lem9  10478  axdc2  10566  fpwwe2lem7  10761  fpwwe2  10767  wunex2  10862  dedekindle  11513  wloglei  11888  uzind4s  13075  seqof2  14243  reuccatpfxs1  14938  shftfn  15269  rexuz3  15560  zsum  15928  fsum  15930  sumss  15934  sumss2  15936  fsumcvg2  15937  fsumser  15940  fsumclf  15948  fsumsplitf  15952  isumless  16058  prodfdiv  16109  cbvprod  16126  cbvprodv  16127  zprod  16148  fprod  16152  fprodntriv  16153  prodss  16158  fprod2dlem  16191  fproddivf  16198  fprodsplitf  16199  rpnnen2lem10  16435  cpnnen  16441  sumeven  16601  sumodd  16602  sadcp1  16669  smupp1  16694  pcmptdvds  17116  prmreclem2  17139  prmreclem5  17142  prmreclem6  17143  prmrec  17144  prmdvdsprmo  17264  iscatd2  17905  initoeu2  18241  yoniso  18509  sgrpidmnd  18978  mndind  19074  eqg0subg  19461  symggen  19735  dprd2d2  20311  srhmsubc  20983  isdrngrd  21074  isdrngrdOLD  21076  lbspss  21408  frlmphl  22142  frlmup1  22159  opsrtoslem1  22419  selvvvval  22506  mdetralt  22978  mdetralt2  22979  mdetunilem2  22983  maducoeval2  23010  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  isclo2  23461  neiptopnei  23505  ptcldmpt  23988  elmptrab  24201  hausflimi  24354  hausflim  24355  alexsubALTlem3  24423  alexsubALTlem4  24424  ptcmplem2  24427  cnextcn  24441  cnextfres1  24442  tgphaus  24491  ustuqtop  24620  utopsnneip  24622  ucncn  24658  nrmmetd  24948  xrhmeo  25322  iscau2  25653  caucfil  25659  cmetcaulem  25664  bcth  25705  vitalilem3  25986  vitali  25989  i1f1lem  26065  itg11  26067  i1fres  26081  mbfi1fseq  26097  mbfi1flim  26099  itg2uba  26119  itg2splitlem  26124  isibl2  26142  cbvitg  26151  cbvitgv  26152  itgss3  26190  dvmptfsum  26350  rolle  26365  elply2  26569  plyexmo  26691  lgamgulmlem2  27414  prmorcht  27562  pclogsum  27599  dchr1  27641  lgsdir  27716  lgsdilem2  27717  lgsdi  27718  lgsne0  27719  lgsquadlem3  27766  lgsquad  27767  2sqlem8  27810  nosupcbv  28116  nosupno  28117  nosupdm  28118  nosupbnd1lem1  28122  noinfcbv  28131  noinfno  28132  noinfdm  28133  nocvxminlem  28197  legval  29104  legov  29105  tglineintmo  29167  tglowdim2ln  29177  ishpg  29294  lnopp2hpgb  29298  hpgerlem  29300  colopp  29304  elplngid  29317  lnincplng  29319  plngcp  29321  plngrot  29325  nhpmirhp  29333  lnperpexs  29367  ragraghl  29403  tgaaddcpbllem2  29407  tgaaddcpbllem3  29408  prlnghpg  29481  prlngmo  29489  tgaltai  29502  axcontlem1  29599  numedglnl  29779  uvtxnbgrvtx  30031  cusgrres  30086  wspniunwspnon  30569  rusgrnumwwlkb0  30620  frgr3vlem2  30932  3vfriswmgrlem  30935  fusgr2wsp2nb  30992  numclwlk2lem2f1o  31037  lpni  31139  pjhthmo  31961  chscllem2  32297  cbvdisjf  33263  2ndresdju  33341  fmptcof2  33349  aciunf1lem  33354  funcnv4mpt  33360  suppovss  33371  fpwrelmapffslem  33420  fsumiunle  33516  gsumwrd2dccatlem  33737  elrspunsn  34083  1arithufdlem3  34182  fedgmullem1  34372  fldextrspunlsp  34417  extdgfialglem2  34436  zarclssn  34616  esumcvg  34829  fiunelros  34918  measiun  34962  bnj1146  35532  bnj1185  35534  bnj1385  35573  bnj1014  35702  bnj1112  35724  bnj1123  35727  bnj1228  35752  bnj1326  35767  bnj1321  35768  bnj1384  35773  bnj1417  35782  bnj1497  35801  reu6f  35820  rmo6  35821  trssfihf  35860  eqhf  35861  fineqvnttrclse  35933  axregscl  35937  setindregs  35939  trssfihfregs  35945  eqhfregs  35946  onvf1odlem2  36073  onvf1odlem3  36074  gonarlem  36367  goalrlem  36369  goalr  36370  mrsubrn  36486  mirimanofffr  36670  elpssmo  36673  dfon2lem6  36765  dfbigcup2  36876  lineintmo  37137  cbvralvw2  37230  cbvrexvw2  37231  cbvrmovw2  37232  cbvreuvw2  37233  cbvmptvw2  37238  cbvprodvw2  37251  cbvrmodavw  37256  cbvreudavw  37257  cbvrabdavw  37265  cbvmptdavw  37271  cbvriotadavw  37274  cbvixpdavw  37282  cbvproddavw  37284  cbvitgdavw  37285  cbvrabdavw2  37289  cbvmptdavw2  37292  cbvriotadavw2  37294  weiunlem  37466  dfttc4  37533  mh-infprim2bi  37550  eleq2w2ALT  38232  bj-idres  38349  mptsnunlem  38529  wl-dfcleq  38705  wl-dfclel  38706  ptrest  38805  poimirlem25  38831  mblfinlem2  38844  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  mbfposadd  38853  itg2addnclem  38857  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anclem7  38885  ftc1anc  38887  areacirclem5  38898  fdc1  38946  inxprnres  39496  fsumshftd  40275  pmapglb  41093  polval2N  41229  osumcllem4N  41282  pexmidlem1N  41293  dih1dimatlem  42652  mapdh9a  43112  mapdh9aOLDN  43113  sticksstones2  43463  fsuppind  43884  fphpd  44089  fphpdo  44090  pellex  44108  setindtrs  44298  dford3lem2  44300  mendlmod  44452  cantnfub  44584  tfsconcat0i  44608  rababg  44836  fsovrfovd  45270  fsovcnvlem  45274  trfr  46216  elunif  46307  iunincfi  46382  cbvmpo2  46385  cbvmpo1  46386  disjf1  46471  wessf1ornlem  46473  disjinfi  46480  supxrleubrnmptf  46734  monoordxr  46765  monoord2xr  46767  fsummulc1f  46856  fsumnncl  46857  fsumf1of  46859  fsumiunss  46860  fsumreclf  46861  fsumlessf  46862  fsumsermpt  46864  fmulcl  46866  fmul01lt1lem2  46870  fprodexp  46879  fprodabs2  46880  climmulf  46889  climexp  46890  climrecf  46894  climinff  46896  climaddf  46900  mullimc  46901  limcperiod  46913  sumnnodd  46915  neglimc  46930  addlimc  46931  climsubmpt  46943  climreclf  46947  climeldmeqmpt  46951  climfveqmpt  46954  fnlimfvre  46957  climfveqf  46963  climfveqmpt3  46965  climeldmeqf  46966  climeqf  46971  climeldmeqmpt3  46972  climinf2  46990  limsupequz  47006  limsupequzmptf  47014  lmbr3  47030  cnrefiisp  47113  cncfshift  47157  fprodcncf  47183  dvmptmulf  47220  dvmptfprod  47228  dvnprodlem1  47229  dvnprodlem3  47231  stoweidlem16  47299  stoweidlem34  47317  stoweidlem62  47345  dirkercncflem2  47387  fourierdlem12  47402  fourierdlem15  47405  fourierdlem34  47424  fourierdlem50  47439  fourierdlem73  47462  fourierdlem94  47483  fourierdlem112  47501  fourierdlem113  47502  intsaluni  47612  sge0lempt  47693  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0iunmpt  47701  sge0ltfirpmpt2  47709  sge0isummpt2  47715  sge0xaddlem2  47717  sge0xadd  47718  meadjiun  47749  voliunsge0lem  47755  meaiuninclem  47763  meaiunincf  47766  meaiuninc3v  47767  meaiuninc3  47768  meaiininclem  47769  meaiininc  47770  isomennd  47814  ovn0lem  47848  sge0hsphoire  47872  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvlelem5  47882  hspmbllem2  47910  hoimbl2  47948  vonhoire  47955  vonioo  47965  vonicc  47968  vonn0ioo2  47973  vonn0icc2  47975  pimincfltioc  47999  salpreimagtlt  48013  smflimlem4  48057  ormkglobd  48160  sinnpoly  48214  rexrsb  48444  ichexmpl2  48825  ichnreuop  48827  sbgoldbm  49155  bgoldbnnsum3prm  49175  tgoldbach  49188  srhmsubcALTV  49695  cbvmpox2  49779  mo0sn  50258  f1omoOLD  50339  isthincd2lem1  50891  thincmo  50894  euendfunc  50992