Theorem eleq1w 2843

Description: Weaker version of eleq1 2848 (but more general than elequ1 2151) not depending on ax-ext 2732 nor df-cleq 2752.

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835

This theorem is used by:  clelsb1  2887  cleqh  2889  nfcjust  2908  nfcr  2912  cleqf  2950  rspw  3239  cbvralvw  3240  cbvrexvw  3241  cbvralfw  3302  cbvralsvw  3313  cbvralf  3345  ralcom2  3362  moel  3385  cbvrmovw  3386  cbvreuvw  3387  cbvrmow  3390  cbvreu  3404  cbvrabv  3422  rabrabi  3430  cbvrabw  3446  nfrab  3448  cbvrab  3449  elrab2w  3649  reu2  3682  reu6  3683  rmo4  3687  reu8  3690  2reu5  3715  csbied  3883  dfssf  3900  difjust  4045  injust  4089  dfss2  4093  unjust  4149  eqeuel  4312  rabeq0w  4336  disj  4402  reldisj  4405  ralidmw  4471  dfif6  4484  rabsnifsb  4679  eluniab  4880  unissb  4900  uniintsn  4944  dfiun2g  4987  dfiunv2  4991  disjxun  5100  cbvmptf  5204  cbvmptfg  5205  cbvmptv  5208  dftr2c  5214  isso2i  5596  dfres2  6035  imai  6074  frpoinsg  6349  tz7.7  6391  fvn0ssdmfun  7079  fmptco  7135  cbvriotaw  7390  cbvriotavw  7391  cbvriota  7394  cbvmpox  7517  cbvmpov  7519  tfis  7870  tfindes  7878  peano5  7909  findes  7916  dfoprab4f  8072  fmpox  8083  fnwe2lem3  8154  xpord2indlem  8171  poseq  8182  soseq  8183  smogt  8383  resixpfo  8972  ixpsnf1o  8974  dom2lem  9027  mapsnend  9072  pw2f1olem  9108  pssnn  9192  ssfi  9196  findcard3  9282  ordiso2  9516  elirrvOLDOLD  9600  cantnflem1d  9696  cantnf  9701  setind  9755  frinsg  9762  tz9.12lem3  9803  scottabf  9946  infxpen  10100  dfac5lem4  10212  dfac12lem2  10230  kmlem14  10249  cfsmolem  10355  sornom  10362  isf32lem9  10446  axdc2  10534  fpwwe2lem7  10729  fpwwe2  10735  wunex2  10830  dedekindle  11481  wloglei  11855  uzind4s  13042  seqof2  14210  reuccatpfxs1  14904  shftfn  15235  rexuz3  15525  zsum  15893  fsum  15895  sumss  15899  sumss2  15901  fsumcvg2  15902  fsumser  15905  fsumclf  15913  fsumsplitf  15917  isumless  16023  prodfdiv  16074  cbvprod  16091  cbvprodv  16092  zprod  16113  fprod  16117  fprodntriv  16118  prodss  16123  fprod2dlem  16156  fproddivf  16163  fprodsplitf  16164  rpnnen2lem10  16400  cpnnen  16406  sumeven  16566  sumodd  16567  sadcp1  16634  smupp1  16659  pcmptdvds  17081  prmreclem2  17104  prmreclem5  17107  prmreclem6  17108  prmrec  17109  prmdvdsprmo  17229  iscatd2  17864  initoeu2  18200  yoniso  18468  sgrpidmnd  18937  mndind  19033  eqg0subg  19420  symggen  19693  dprd2d2  20269  srhmsubc  20941  isdrngrd  21032  isdrngrdOLD  21034  lbspss  21366  frlmphl  22096  frlmup1  22113  opsrtoslem1  22373  selvvvval  22460  mdetralt  22932  mdetralt2  22933  mdetunilem2  22937  maducoeval2  22964  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  isclo2  23415  neiptopnei  23459  ptcldmpt  23942  elmptrab  24155  hausflimi  24308  hausflim  24309  alexsubALTlem3  24377  alexsubALTlem4  24378  ptcmplem2  24381  cnextcn  24395  cnextfres1  24396  tgphaus  24445  ustuqtop  24574  utopsnneip  24576  ucncn  24612  nrmmetd  24902  xrhmeo  25276  iscau2  25607  caucfil  25613  cmetcaulem  25618  bcth  25659  vitalilem3  25940  vitali  25943  i1f1lem  26019  itg11  26021  i1fres  26035  mbfi1fseq  26051  mbfi1flim  26053  itg2uba  26073  itg2splitlem  26078  isibl2  26096  cbvitg  26105  cbvitgv  26106  itgss3  26144  dvmptfsum  26304  rolle  26319  elply2  26523  plyexmo  26645  lgamgulmlem2  27366  prmorcht  27514  pclogsum  27551  dchr1  27593  lgsdir  27668  lgsdilem2  27669  lgsdi  27670  lgsne0  27671  lgsquadlem3  27718  lgsquad  27719  2sqlem8  27762  nosupcbv  28068  nosupno  28069  nosupdm  28070  nosupbnd1lem1  28074  noinfcbv  28083  noinfno  28084  noinfdm  28085  nocvxminlem  28149  legval  29056  legov  29057  tglineintmo  29119  tglowdim2ln  29129  ishpg  29246  lnopp2hpgb  29250  hpgerlem  29252  colopp  29256  elplngid  29269  lnincplng  29271  plngcp  29273  plngrot  29277  nhpmirhp  29285  lnperpexs  29319  ragraghl  29355  tgaaddcpbllem2  29359  tgaaddcpbllem3  29360  prlnghpg  29433  prlngmo  29441  tgaltai  29454  axcontlem1  29551  numedglnl  29731  uvtxnbgrvtx  29983  cusgrres  30038  wspniunwspnon  30521  rusgrnumwwlkb0  30572  frgr3vlem2  30884  3vfriswmgrlem  30887  fusgr2wsp2nb  30944  numclwlk2lem2f1o  30989  lpni  31091  pjhthmo  31913  chscllem2  32249  cbvdisjf  33216  2ndresdju  33294  fmptcof2  33302  aciunf1lem  33307  funcnv4mpt  33313  suppovss  33325  fpwrelmapffslem  33374  fsumiunle  33470  gsumwrd2dccatlem  33688  elrspunsn  34029  1arithufdlem3  34128  fedgmullem1  34311  fldextrspunlsp  34356  extdgfialglem2  34375  zarclssn  34555  esumcvg  34768  fiunelros  34857  measiun  34901  bnj1146  35471  bnj1185  35473  bnj1385  35512  bnj1014  35641  bnj1112  35663  bnj1123  35666  bnj1228  35691  bnj1326  35706  bnj1321  35707  bnj1384  35712  bnj1417  35721  bnj1497  35740  reu6f  35759  rmo6  35760  trssfir1om  35795  r1omhfb  35796  fineqvnttrclse  35860  axregscl  35864  setindregs  35866  trssfir1omregs  35872  r1omhfbregs  35873  onvf1odlem2  35983  onvf1odlem3  35984  gonarlem  36277  goalrlem  36279  goalr  36280  mrsubrn  36396  dfon2lem6  36674  dfbigcup2  36785  lineintmo  37046  cbvralvw2  37139  cbvrexvw2  37140  cbvrmovw2  37141  cbvreuvw2  37142  cbvmptvw2  37147  cbvprodvw2  37160  cbvrmodavw  37165  cbvreudavw  37166  cbvrabdavw  37174  cbvmptdavw  37180  cbvriotadavw  37183  cbvixpdavw  37191  cbvproddavw  37193  cbvitgdavw  37194  cbvrabdavw2  37198  cbvmptdavw2  37201  cbvriotadavw2  37203  weiunlem  37375  dfttc4  37442  mh-infprim2bi  37459  eleq2w2ALT  38098  bj-idres  38218  mptsnunlem  38398  wl-dfcleq  38574  wl-dfclel  38575  ptrest  38674  poimirlem25  38700  mblfinlem2  38713  mblfinlem3  38714  mblfinlem4  38715  ismblfin  38716  mbfposadd  38722  itg2addnclem  38726  ftc1anclem5  38752  ftc1anclem6  38753  ftc1anclem7  38754  ftc1anc  38756  areacirclem5  38767  fdc1  38817  inxprnres  39367  fsumshftd  40146  pmapglb  40964  polval2N  41100  osumcllem4N  41153  pexmidlem1N  41164  dih1dimatlem  42523  mapdh9a  42983  mapdh9aOLDN  42984  sticksstones2  43334  fsuppind  43755  fphpd  43960  fphpdo  43961  pellex  43979  setindtrs  44169  dford3lem2  44171  mendlmod  44328  cantnfub  44460  tfsconcat0i  44484  rababg  44712  fsovrfovd  45146  fsovcnvlem  45150  trfr  46088  elunif  46169  iunincfi  46245  cbvmpo2  46248  cbvmpo1  46249  disjf1  46334  wessf1ornlem  46336  disjinfi  46343  supxrleubrnmptf  46597  monoordxr  46628  monoord2xr  46630  fsummulc1f  46719  fsumnncl  46720  fsumf1of  46722  fsumiunss  46723  fsumreclf  46724  fsumlessf  46725  fsumsermpt  46727  fmulcl  46729  fmul01lt1lem2  46733  fprodexp  46742  fprodabs2  46743  climmulf  46752  climexp  46753  climrecf  46757  climinff  46759  climaddf  46763  mullimc  46764  limcperiod  46776  sumnnodd  46778  neglimc  46793  addlimc  46794  climsubmpt  46806  climreclf  46810  climeldmeqmpt  46814  climfveqmpt  46817  fnlimfvre  46820  climfveqf  46826  climfveqmpt3  46828  climeldmeqf  46829  climeqf  46834  climeldmeqmpt3  46835  climinf2  46853  limsupequz  46869  limsupequzmptf  46877  lmbr3  46893  cnrefiisp  46976  cncfshift  47020  fprodcncf  47046  dvmptmulf  47083  dvmptfprod  47091  dvnprodlem1  47092  dvnprodlem3  47094  stoweidlem16  47162  stoweidlem34  47180  stoweidlem62  47208  dirkercncflem2  47250  fourierdlem12  47265  fourierdlem15  47268  fourierdlem34  47287  fourierdlem50  47302  fourierdlem73  47325  fourierdlem94  47346  fourierdlem112  47364  fourierdlem113  47365  intsaluni  47475  sge0lempt  47556  sge0iunmptlemfi  47559  sge0iunmptlemre  47561  sge0iunmpt  47564  sge0ltfirpmpt2  47572  sge0isummpt2  47578  sge0xaddlem2  47580  sge0xadd  47581  meadjiun  47612  voliunsge0lem  47618  meaiuninclem  47626  meaiunincf  47629  meaiuninc3v  47630  meaiuninc3  47631  meaiininclem  47632  meaiininc  47633  isomennd  47677  ovn0lem  47711  sge0hsphoire  47735  hoidmvlelem1  47741  hoidmvlelem2  47742  hoidmvlelem3  47743  hoidmvlelem5  47745  hspmbllem2  47773  hoimbl2  47811  vonhoire  47818  vonioo  47828  vonicc  47831  vonn0ioo2  47836  vonn0icc2  47838  pimincfltioc  47862  salpreimagtlt  47876  smflimlem4  47920  ormkglobd  48023  sinnpoly  48077  rexrsb  48307  ichexmpl2  48688  ichnreuop  48690  sbgoldbm  49018  bgoldbnnsum3prm  49038  tgoldbach  49051  srhmsubcALTV  49558  cbvmpox2  49584  mo0sn  50063  f1omoOLD  50144  isthincd2lem1  50696  thincmo  50699  euendfunc  50797