Theorem eleq1w 2848

Description: Weaker version of eleq1 2853 (but more general than elequ1 2153) not depending on ax-ext 2737 nor df-cleq 2757.

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

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

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 2148

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

This theorem is used by:  clelsb1  2892  cleqh  2894  nfcjust  2913  nfcr  2917  cleqf  2955  rspw  3244  cbvralvw  3245  cbvrexvw  3246  cbvralfw  3307  cbvralsvw  3318  cbvralf  3351  ralcom2  3368  moel  3391  cbvrmovw  3392  cbvreuvw  3393  cbvrmow  3396  cbvreu  3410  cbvrabv  3428  rabrabi  3437  cbvrabw  3453  nfrab  3455  cbvrab  3456  elrab2w  3657  reu2  3690  reu6  3691  rmo4  3695  reu8  3698  2reu5  3723  csbied  3890  difjust  3908  unjust  3910  injust  3912  dfss2  3924  dfssf  3929  eqeuel  4320  rabeq0w  4344  disj  4410  reldisj  4413  ralidmw  4479  dfif6  4492  rabsnifsb  4690  eluniab  4888  unissb  4908  uniintsn  4952  dfiun2g  4996  dfiunv2  5000  disjxun  5109  cbvmptf  5213  cbvmptfg  5214  cbvmptv  5217  dftr2c  5223  isso2i  5608  dfres2  6045  imai  6078  frpoinsg  6348  tz7.7  6390  fvn0ssdmfun  7073  fmptco  7129  cbvriotaw  7385  cbvriotavw  7386  cbvriota  7389  cbvmpox  7512  cbvmpov  7514  tfis  7857  tfindes  7865  peano5  7896  findes  7903  dfoprab4f  8059  fmpox  8070  xpord2indlem  8149  poseq  8160  soseq  8161  smogt  8360  resixpfo  8940  ixpsnf1o  8942  dom2lem  8995  mapsnend  9040  pw2f1olem  9076  pssnn  9160  ssfi  9164  findcard3  9250  ordiso2  9484  elirrvOLDOLD  9568  cantnflem1d  9664  cantnf  9669  setind  9723  frinsg  9730  tz9.12lem3  9768  scottabf  9875  infxpen  10014  dfac5lem4  10126  dfac12lem2  10144  kmlem14  10163  cfsmolem  10269  sornom  10276  isf32lem9  10360  axdc2  10448  fpwwe2lem7  10637  fpwwe2  10643  wunex2  10738  dedekindle  11389  wloglei  11761  uzind4s  12948  seqof2  14114  reuccatpfxs1  14806  shftfn  15134  rexuz3  15424  zsum  15792  fsum  15794  sumss  15798  sumss2  15800  fsumcvg2  15801  fsumser  15804  fsumclf  15812  fsumsplitf  15816  isumless  15922  prodfdiv  15973  cbvprod  15990  cbvprodv  15991  zprod  16014  fprod  16018  fprodntriv  16019  prodss  16024  fprod2dlem  16057  fproddivf  16064  fprodsplitf  16065  rpnnen2lem10  16301  cpnnen  16307  sumeven  16467  sumodd  16468  sadcp1  16535  smupp1  16560  pcmptdvds  16976  prmreclem2  16999  prmreclem5  17002  prmreclem6  17003  prmrec  17004  prmdvdsprmo  17124  iscatd2  17759  initoeu2  18095  yoniso  18363  sgrpidmnd  18829  mndind  18924  eqg0subg  19311  symggen  19584  dprd2d2  20160  srhmsubc  20829  isdrngrd  20919  isdrngrdOLD  20921  lbspss  21253  frlmphl  21981  frlmup1  21998  opsrtoslem1  22256  selvvvval  22343  mdetralt  22815  mdetralt2  22816  mdetunilem2  22820  maducoeval2  22847  chfacfscmulgsum  23067  chfacfpmmulgsum  23071  isclo2  23295  neiptopnei  23339  ptcldmpt  23822  elmptrab  24035  hausflimi  24188  hausflim  24189  alexsubALTlem3  24257  alexsubALTlem4  24258  ptcmplem2  24261  cnextcn  24275  cnextfres1  24276  tgphaus  24325  ustuqtop  24454  utopsnneip  24456  ucncn  24492  nrmmetd  24782  xrhmeo  25156  iscau2  25487  caucfil  25493  cmetcaulem  25498  bcth  25539  vitalilem3  25820  vitali  25823  i1f1lem  25899  itg11  25901  i1fres  25915  mbfi1fseq  25931  mbfi1flim  25933  itg2uba  25953  itg2splitlem  25958  isibl2  25976  cbvitg  25986  cbvitgv  25987  itgss3  26025  dvmptfsum  26185  rolle  26200  elply2  26404  plyexmo  26525  lgamgulmlem2  27245  prmorcht  27393  pclogsum  27430  dchr1  27472  lgsdir  27547  lgsdilem2  27548  lgsdi  27549  lgsne0  27550  lgsquadlem3  27597  lgsquad  27598  2sqlem8  27641  nosupcbv  27917  nosupno  27918  nosupdm  27919  nosupbnd1lem1  27923  noinfcbv  27932  noinfno  27933  noinfdm  27934  nocvxminlem  27998  legval  28904  legov  28905  tglineintmo  28966  tglowdim2ln  28976  ishpg  29092  lnopp2hpgb  29096  hpgerlem  29098  colopp  29102  elplngid  29115  lnincplng  29117  plngcp  29119  plngrot  29123  nhpmirhp  29131  lnperpexs  29165  ragraghl  29200  tgaaddcpbllem2  29204  tgaaddcpbllem3  29205  prlnghpg  29251  prlngmo  29259  tgaltai  29272  axcontlem1  29369  numedglnl  29549  uvtxnbgrvtx  29801  cusgrres  29856  wspniunwspnon  30339  rusgrnumwwlkb0  30390  frgr3vlem2  30696  3vfriswmgrlem  30699  fusgr2wsp2nb  30756  numclwlk2lem2f1o  30801  lpni  30903  pjhthmo  31725  chscllem2  32061  cbvdisjf  32987  2ndresdju  33065  fmptcof2  33073  aciunf1lem  33078  funcnv4mpt  33084  suppovss  33097  fpwrelmapffslem  33147  fsumiunle  33243  gsumwrd2dccatlem  33461  elrspunsn  33801  1arithufdlem3  33900  fedgmullem1  34083  fldextrspunlsp  34128  extdgfialglem2  34147  zarclssn  34327  esumcvg  34540  fiunelros  34629  measiun  34673  bnj1146  35244  bnj1185  35246  bnj1385  35285  bnj1014  35414  bnj1112  35436  bnj1123  35439  bnj1228  35464  bnj1326  35479  bnj1321  35480  bnj1384  35485  bnj1417  35494  bnj1497  35513  trssfir1om  35565  r1omhfb  35566  fineqvnttrclse  35594  axregscl  35598  setindregs  35600  trssfir1omregs  35606  r1omhfbregs  35607  onvf1odlem2  35645  onvf1odlem3  35646  gonarlem  35923  goalrlem  35925  goalr  35926  mrsubrn  36042  dfon2lem6  36315  dfbigcup2  36426  lineintmo  36686  cbvralvw2  36795  cbvrexvw2  36796  cbvrmovw2  36797  cbvreuvw2  36798  cbvmptvw2  36803  cbvprodvw2  36816  cbvrmodavw  36821  cbvreudavw  36822  cbvrabdavw  36830  cbvmptdavw  36836  cbvriotadavw  36839  cbvixpdavw  36847  cbvproddavw  36849  cbvitgdavw  36850  cbvrabdavw2  36854  cbvmptdavw2  36857  cbvriotadavw2  36859  weiunlem  37031  dfttc4  37098  mh-infprim2bi  37115  eleq2w2ALT  37740  bj-idres  37861  mptsnunlem  38041  wl-dfcleq  38217  wl-dfclel  38218  ptrest  38327  poimirlem25  38353  mblfinlem2  38366  mblfinlem3  38367  mblfinlem4  38368  ismblfin  38369  mbfposadd  38375  itg2addnclem  38379  ftc1anclem5  38405  ftc1anclem6  38406  ftc1anclem7  38407  ftc1anc  38409  areacirclem5  38420  fdc1  38455  inxprnres  39005  fsumshftd  39784  pmapglb  40602  polval2N  40738  osumcllem4N  40791  pexmidlem1N  40802  dih1dimatlem  42161  mapdh9a  42621  mapdh9aOLDN  42622  sticksstones2  42972  fsuppind  43380  fphpd  43601  fphpdo  43602  pellex  43620  setindtrs  43810  dford3lem2  43812  fnwe2lem2  43836  mendlmod  43974  cantnfub  44106  tfsconcat0i  44130  rababg  44358  fsovrfovd  44793  fsovcnvlem  44797  trfr  45729  elunif  45794  iunincfi  45870  cbvmpo2  45873  cbvmpo1  45874  disjf1  45959  wessf1ornlem  45961  disjinfi  45968  supxrleubrnmptf  46223  monoordxr  46254  monoord2xr  46256  fsummulc1f  46345  fsumnncl  46346  fsumf1of  46348  fsumiunss  46349  fsumreclf  46350  fsumlessf  46351  fsumsermpt  46353  fmulcl  46355  fmul01lt1lem2  46359  fprodexp  46368  fprodabs2  46369  climmulf  46378  climexp  46379  climrecf  46383  climinff  46385  climaddf  46389  mullimc  46390  limcperiod  46402  sumnnodd  46404  neglimc  46419  addlimc  46420  climsubmpt  46432  climreclf  46436  climeldmeqmpt  46440  climfveqmpt  46443  fnlimfvre  46446  climfveqf  46452  climfveqmpt3  46454  climeldmeqf  46455  climeqf  46460  climeldmeqmpt3  46461  climinf2  46479  limsupequz  46495  limsupequzmptf  46503  lmbr3  46519  cnrefiisp  46602  cncfshift  46646  fprodcncf  46672  dvmptmulf  46709  dvmptfprod  46717  dvnprodlem1  46718  dvnprodlem3  46720  stoweidlem16  46788  stoweidlem34  46806  stoweidlem62  46834  dirkercncflem2  46876  fourierdlem12  46891  fourierdlem15  46894  fourierdlem34  46913  fourierdlem50  46928  fourierdlem73  46951  fourierdlem94  46972  fourierdlem112  46990  fourierdlem113  46991  intsaluni  47101  sge0lempt  47182  sge0iunmptlemfi  47185  sge0iunmptlemre  47187  sge0iunmpt  47190  sge0ltfirpmpt2  47198  sge0isummpt2  47204  sge0xaddlem2  47206  sge0xadd  47207  meadjiun  47238  voliunsge0lem  47244  meaiuninclem  47252  meaiunincf  47255  meaiuninc3v  47256  meaiuninc3  47257  meaiininclem  47258  meaiininc  47259  isomennd  47303  ovn0lem  47337  sge0hsphoire  47361  hoidmvlelem1  47367  hoidmvlelem2  47368  hoidmvlelem3  47369  hoidmvlelem5  47371  hspmbllem2  47399  hoimbl2  47437  vonhoire  47444  vonioo  47454  vonicc  47457  vonn0ioo2  47462  vonn0icc2  47464  pimincfltioc  47488  salpreimagtlt  47502  smflimlem4  47546  ormkglobd  47649  sinnpoly  47686  rexrsb  47895  ichexmpl2  48277  ichnreuop  48279  sbgoldbm  48607  bgoldbnnsum3prm  48627  tgoldbach  48640  srhmsubcALTV  49147  cbvmpox2  49173  mo0sn  49651  f1omoOLD  49729  isthincd2lem1  50260  thincmo  50263  euendfunc  50361