Theorem eleq1w 2820

Description: Weaker version of eleq1 2825 (but more general than elequ1 2121) not depending on ax-ext 2709 nor df-cleq 2729.

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  clelsb1  2864  cleqh  2866  nfcjust  2885  nfcr  2889  cleqf  2928  rspw  3214  cbvralvw  3215  cbvrexvw  3216  cbvralfw  3277  cbvralsvw  3288  cbvralf  3331  ralcom2  3348  moel  3371  cbvrmovw  3372  cbvreuvw  3373  cbvrmow  3376  cbvreu  3392  cbvrabv  3410  rabrabi  3419  cbvrabw  3435  cbvrabwOLD  3436  nfrab  3439  cbvrab  3440  elrab2w  3651  reu2  3684  reu6  3685  rmo4  3689  reu8  3692  2reu5  3717  ruOLD  3740  csbied  3886  difjust  3904  unjust  3906  injust  3908  dfss2  3920  dfssf  3925  dfdif3OLD  4071  eqeuel  4318  rabeq0w  4340  disj  4403  reldisj  4406  ralidmw  4470  dfif6  4483  rabsnifsb  4680  eluniab  4878  unissb  4897  uniintsn  4941  dfiun2g  4986  dfiunv2  4990  disjxun  5097  cbvmptf  5199  cbvmptfg  5200  cbvmptv  5203  dftr2c  5209  isso2i  5570  dfres2  6001  imai  6034  frpoinsg  6302  tz7.7  6344  fvn0ssdmfun  7021  fmptco  7076  cbvriotaw  7326  cbvriotavw  7327  cbvriota  7330  cbvmpox  7453  cbvmpov  7455  tfis  7799  tfindes  7807  peano5  7837  findes  7844  dfoprab4f  8002  fmpox  8013  xpord2indlem  8091  poseq  8102  soseq  8103  smogt  8301  resixpfo  8878  ixpsnf1o  8880  dom2lem  8933  mapsnend  8977  pw2f1olem  9013  pssnn  9097  ssfi  9101  findcard3  9187  ordiso2  9424  elirrvOLD  9507  cantnflem1d  9601  cantnf  9606  setind  9660  frinsg  9667  tz9.12lem3  9705  infxpen  9928  dfac5lem4  10040  dfac12lem2  10059  kmlem14  10078  cfsmolem  10184  sornom  10191  isf32lem9  10275  axdc2  10363  fpwwe2lem7  10552  fpwwe2  10558  wunex2  10653  dedekindle  11301  wloglei  11673  uzind4s  12825  seqof2  13987  reuccatpfxs1  14674  shftfn  15000  rexuz3  15276  zsum  15645  fsum  15647  sumss  15651  sumss2  15653  fsumcvg2  15654  fsumser  15657  fsumclf  15665  fsumsplitf  15669  isumless  15772  prodfdiv  15823  cbvprod  15840  cbvprodv  15841  zprod  15864  fprod  15868  fprodntriv  15869  prodss  15874  fprod2dlem  15907  fproddivf  15914  fprodsplitf  15915  rpnnen2lem10  16152  cpnnen  16158  sumeven  16318  sumodd  16319  sadcp1  16386  smupp1  16411  pcmptdvds  16826  prmreclem2  16849  prmreclem5  16852  prmreclem6  16853  prmrec  16854  prmdvdsprmo  16974  iscatd2  17608  initoeu2  17944  yoniso  18212  sgrpidmnd  18668  mndind  18757  eqg0subg  19129  symggen  19403  dprd2d2  19979  srhmsubc  20617  isdrngrd  20703  isdrngrdOLD  20705  lbspss  21038  frlmphl  21740  frlmup1  21757  opsrtoslem1  22014  mdetralt  22556  mdetralt2  22557  mdetunilem2  22561  maducoeval2  22588  chfacfscmulgsum  22808  chfacfpmmulgsum  22812  isclo2  23036  neiptopnei  23080  ptcldmpt  23562  elmptrab  23775  hausflimi  23928  hausflim  23929  alexsubALTlem3  23997  alexsubALTlem4  23998  ptcmplem2  24001  cnextcn  24015  cnextfres1  24016  tgphaus  24065  ustuqtop  24194  utopsnneip  24196  ucncn  24232  nrmmetd  24522  xrhmeo  24904  iscau2  25237  caucfil  25243  cmetcaulem  25248  bcth  25289  vitalilem3  25571  vitali  25574  i1f1lem  25650  itg11  25652  i1fres  25666  mbfi1fseq  25682  mbfi1flim  25684  itg2uba  25704  itg2splitlem  25709  isibl2  25727  cbvitg  25737  cbvitgv  25738  itgss3  25776  dvmptfsum  25939  rolle  25954  elply2  26161  plyexmo  26281  lgamgulmlem2  27000  prmorcht  27148  pclogsum  27186  dchr1  27228  lgsdir  27303  lgsdilem2  27304  lgsdi  27305  lgsne0  27306  lgsquadlem3  27353  lgsquad  27354  2sqlem8  27397  nosupcbv  27674  nosupno  27675  nosupdm  27676  nosupbnd1lem1  27680  noinfcbv  27689  noinfno  27690  noinfdm  27691  nocvxminlem  27754  legval  28639  legov  28640  tglineintmo  28697  tglowdim2ln  28706  ishpg  28814  lnopp2hpgb  28818  hpgerlem  28820  colopp  28824  axcontlem1  29020  numedglnl  29200  uvtxnbgrvtx  29449  cusgrres  29505  wspniunwspnon  29979  rusgrnumwwlkb0  30030  frgr3vlem2  30332  3vfriswmgrlem  30335  fusgr2wsp2nb  30392  numclwlk2lem2f1o  30437  lpni  30538  pjhthmo  31360  chscllem2  31696  cbvdisjf  32628  2ndresdju  32709  fmptcof2  32717  aciunf1lem  32722  funcnv4mpt  32728  suppovss  32741  fpwrelmapffslem  32792  fsumiunle  32891  gsumwrd2dccatlem  33140  elrspunsn  33491  1arithufdlem3  33608  fedgmullem1  33767  fldextrspunlsp  33812  extdgfialglem2  33831  zarclssn  34011  esumcvg  34224  fiunelros  34312  measiun  34356  bnj1146  34928  bnj1185  34930  bnj1385  34969  bnj1014  35098  bnj1112  35120  bnj1123  35123  bnj1228  35148  bnj1326  35163  bnj1321  35164  bnj1384  35169  bnj1417  35178  bnj1497  35197  trssfir1om  35248  r1omhfb  35249  fineqvnttrclse  35261  axregscl  35265  setindregs  35267  trssfir1omregs  35273  r1omhfbregs  35274  onvf1odlem2  35279  onvf1odlem3  35280  gonarlem  35569  goalrlem  35571  goalr  35572  mrsubrn  35688  dfon2lem6  35961  dfbigcup2  36072  lineintmo  36332  cbvralvw2  36401  cbvrexvw2  36402  cbvrmovw2  36403  cbvreuvw2  36404  cbvmptvw2  36409  cbvprodvw2  36422  cbvrmodavw  36427  cbvreudavw  36428  cbvrabdavw  36436  cbvmptdavw  36442  cbvriotadavw  36445  cbvixpdavw  36453  cbvproddavw  36455  cbvitgdavw  36456  cbvrabdavw2  36460  cbvmptdavw2  36463  cbvriotadavw2  36465  weiunlem2  36638  eleq2w2ALT  37223  bj-idres  37336  mptsnunlem  37514  ptrest  37791  poimirlem25  37817  mblfinlem2  37830  mblfinlem3  37831  mblfinlem4  37832  ismblfin  37833  mbfposadd  37839  itg2addnclem  37843  ftc1anclem5  37869  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anc  37873  areacirclem5  37884  fdc1  37918  inxprnres  38470  fsumshftd  39249  pmapglb  40067  polval2N  40203  osumcllem4N  40256  pexmidlem1N  40267  dih1dimatlem  41626  mapdh9a  42086  mapdh9aOLDN  42087  sticksstones2  42438  selvvvval  42864  fsuppind  42869  fphpd  43094  fphpdo  43095  pellex  43113  setindtrs  43303  dford3lem2  43305  fnwe2lem2  43329  mendlmod  43467  cantnfub  43599  tfsconcat0i  43623  rababg  43851  fsovrfovd  44286  fsovcnvlem  44290  scottabf  44517  trfr  45239  elunif  45297  iunincfi  45374  cbvmpo2  45377  cbvmpo1  45378  disjf1  45463  wessf1ornlem  45465  disjinfi  45472  supxrleubrnmptf  45731  monoordxr  45762  monoord2xr  45764  fsummulc1f  45853  fsumnncl  45854  fsumf1of  45856  fsumiunss  45857  fsumreclf  45858  fsumlessf  45859  fsumsermpt  45861  fmulcl  45863  fmul01lt1lem2  45867  fprodexp  45876  fprodabs2  45877  climmulf  45886  climexp  45887  climrecf  45891  climinff  45893  climaddf  45897  mullimc  45898  limcperiod  45910  sumnnodd  45912  neglimc  45927  addlimc  45928  climsubmpt  45940  climreclf  45944  climeldmeqmpt  45948  climfveqmpt  45951  fnlimfvre  45954  climfveqf  45960  climfveqmpt3  45962  climeldmeqf  45963  climeqf  45968  climeldmeqmpt3  45969  climinf2  45987  limsupequz  46003  limsupequzmptf  46011  lmbr3  46027  cnrefiisp  46110  cncfshift  46154  fprodcncf  46180  dvmptmulf  46217  dvmptfprod  46225  dvnprodlem1  46226  dvnprodlem3  46228  stoweidlem16  46296  stoweidlem34  46314  stoweidlem62  46342  dirkercncflem2  46384  fourierdlem12  46399  fourierdlem15  46402  fourierdlem34  46421  fourierdlem50  46436  fourierdlem73  46459  fourierdlem94  46480  fourierdlem112  46498  fourierdlem113  46499  intsaluni  46609  sge0lempt  46690  sge0iunmptlemfi  46693  sge0iunmptlemre  46695  sge0iunmpt  46698  sge0ltfirpmpt2  46706  sge0isummpt2  46712  sge0xaddlem2  46714  sge0xadd  46715  meadjiun  46746  voliunsge0lem  46752  meaiuninclem  46760  meaiunincf  46763  meaiuninc3v  46764  meaiuninc3  46765  meaiininclem  46766  meaiininc  46767  isomennd  46811  ovn0lem  46845  sge0hsphoire  46869  hoidmvlelem1  46875  hoidmvlelem2  46876  hoidmvlelem3  46877  hoidmvlelem5  46879  hspmbllem2  46907  hoimbl2  46945  vonhoire  46952  vonioo  46962  vonicc  46965  vonn0ioo2  46970  vonn0icc2  46972  pimincfltioc  46996  salpreimagtlt  47010  smflimlem4  47054  ormkglobd  47155  sinnpoly  47173  rexrsb  47382  ichexmpl2  47752  ichnreuop  47754  sbgoldbm  48066  bgoldbnnsum3prm  48086  tgoldbach  48099  srhmsubcALTV  48607  cbvmpox2  48618  mo0sn  49097  f1omoOLD  49175  isthincd2lem1  49706  thincmo  49709  euendfunc  49807