Theorem eleq1w 2812

Description: Weaker version of eleq1 2817 (but more general than elequ1 2106) not depending on ax-ext 2699 nor df-cleq 2720.

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∃wex 1774   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-clel 2806

This theorem is referenced by:  clelsb1  2856  cleqh  2859  nfcjust  2880  nfcr  2884  nfcriOLD  2889  nfcriOLDOLD  2890  cleqf  2930  rspw  3229  cbvralvw  3230  cbvrexvw  3231  cbvralfw  3297  cbvralfwOLD  3316  cbvralf  3352  ralcom2  3369  moel  3394  cbvrmovw  3395  cbvreuvw  3396  moelOLD  3397  cbvrmow  3401  cbvreuwOLD  3408  cbvreu  3420  cbvrabv  3438  rabrabi  3446  cbvrabw  3463  nfrab  3468  cbvrab  3469  reu2  3719  reu6  3720  rmo4  3724  reu8  3727  2reu5  3752  ru  3774  csbied  3928  difjust  3947  unjust  3949  injust  3951  dfss2f  3968  dfdif3  4110  eqeuel  4358  rabeq0w  4379  disj  4443  reldisj  4447  ralidmw  4503  dfif6  4527  rabsnifsb  4722  eluniab  4917  unissb  4937  elintabOLD  4957  uniintsn  4985  dfiun2g  5027  dfiunv2  5032  disjxun  5140  cbvmptf  5251  cbvmptfg  5252  cbvmptv  5255  dftr2c  5262  isso2i  5619  dfres2  6039  imai  6071  frpoinsg  6343  wfisgOLD  6354  tz7.7  6389  fvn0ssdmfun  7078  fmptco  7132  cbvriotaw  7379  cbvriotavw  7380  cbvriota  7384  cbvmpox  7507  tfis  7853  tfindes  7861  peano5  7893  findes  7902  dfoprab4f  8054  fmpox  8065  xpord2indlem  8146  poseq  8157  soseq  8158  wfrlem10OLD  8332  smogt  8381  resixpfo  8948  ixpsnf1o  8950  dom2lem  9006  mapsnend  9054  pw2f1olem  9094  pssnn  9186  ssfi  9191  findcard3  9303  findcard3OLD  9304  ordiso2  9532  elirrv  9613  cantnflem1d  9705  cantnf  9710  setind  9751  frinsg  9768  tz9.12lem3  9806  infxpen  10031  dfac12lem2  10161  kmlem14  10180  cfsmolem  10287  sornom  10294  isf32lem9  10378  axdc2  10466  fpwwe2lem7  10654  fpwwe2  10660  wunex2  10755  dedekindle  11402  wloglei  11770  uzind4s  12916  seqof2  14051  reuccatpfxs1  14723  shftfn  15046  rexuz3  15321  zsum  15690  fsum  15692  sumss  15696  sumss2  15698  fsumcvg2  15699  fsumser  15702  fsumclf  15710  fsumsplitf  15714  isumless  15817  prodfdiv  15868  cbvprod  15885  zprod  15907  fprod  15911  fprodntriv  15912  prodss  15917  fprod2dlem  15950  fproddivf  15957  fprodsplitf  15958  rpnnen2lem10  16193  cpnnen  16199  sumeven  16357  sumodd  16358  sadcp1  16423  smupp1  16448  pcmptdvds  16856  prmreclem2  16879  prmreclem5  16882  prmreclem6  16883  prmrec  16884  prmdvdsprmo  17004  iscatd2  17654  initoeu2  17998  yoniso  18270  sgrpidmnd  18692  mndind  18773  eqg0subg  19144  symggen  19418  dprd2d2  19994  srhmsubc  20606  isdrngrd  20651  isdrngrdOLD  20653  lbspss  20960  frlmphl  21708  frlmup1  21725  opsrtoslem1  21992  mdetralt  22503  mdetralt2  22504  mdetunilem2  22508  maducoeval2  22535  chfacfscmulgsum  22755  chfacfpmmulgsum  22759  isclo2  22985  neiptopnei  23029  ptcldmpt  23511  elmptrab  23724  hausflimi  23877  hausflim  23878  alexsubALTlem3  23946  alexsubALTlem4  23947  ptcmplem2  23950  cnextcn  23964  cnextfres1  23965  tgphaus  24014  ustuqtop  24144  utopsnneip  24146  ucncn  24183  nrmmetd  24476  xrhmeo  24864  iscau2  25198  caucfil  25204  cmetcaulem  25209  bcth  25250  vitalilem3  25532  vitali  25535  i1f1lem  25611  itg11  25613  i1fres  25628  mbfi1fseq  25644  mbfi1flim  25646  itg2uba  25666  itg2splitlem  25671  isibl2  25689  cbvitg  25698  itgss3  25737  dvmptfsum  25900  rolle  25915  elply2  26123  plyexmo  26241  lgamgulmlem2  26955  prmorcht  27103  pclogsum  27141  dchr1  27183  lgsdir  27258  lgsdilem2  27259  lgsdi  27260  lgsne0  27261  lgsquadlem3  27308  lgsquad  27309  2sqlem8  27352  nosupcbv  27628  nosupno  27629  nosupdm  27630  nosupbnd1lem1  27634  noinfcbv  27643  noinfno  27644  noinfdm  27645  nocvxminlem  27703  legval  28381  legov  28382  tglineintmo  28439  tglowdim2ln  28448  ishpg  28556  lnopp2hpgb  28560  hpgerlem  28562  colopp  28566  axcontlem1  28768  numedglnl  28950  uvtxnbgrvtx  29199  cusgrres  29255  wspniunwspnon  29727  rusgrnumwwlkb0  29775  frgr3vlem2  30077  3vfriswmgrlem  30080  fusgr2wsp2nb  30137  numclwlk2lem2f1o  30182  lpni  30283  pjhthmo  31105  chscllem2  31441  cbvdisjf  32354  2ndresdju  32428  fmptcof2  32436  aciunf1lem  32441  funcnv4mpt  32448  suppovss  32458  fpwrelmapffslem  32508  fsumiunle  32586  elrspunsn  33139  fedgmullem1  33317  zarclssn  33468  esumcvg  33699  fiunelros  33787  measiun  33831  bnj1146  34416  bnj1185  34418  bnj1385  34457  bnj1014  34586  bnj1112  34608  bnj1123  34611  bnj1228  34636  bnj1326  34651  bnj1321  34652  bnj1384  34657  bnj1417  34666  bnj1497  34685  gonarlem  34998  goalrlem  35000  goalr  35001  mrsubrn  35117  dfon2lem6  35378  dfbigcup2  35489  lineintmo  35747  eleq2w2ALT  36520  bj-idres  36633  mptsnunlem  36811  ptrest  37086  poimirlem25  37112  mblfinlem2  37125  mblfinlem3  37126  mblfinlem4  37127  ismblfin  37128  mbfposadd  37134  itg2addnclem  37138  ftc1anclem5  37164  ftc1anclem6  37165  ftc1anclem7  37166  ftc1anc  37168  areacirclem5  37179  fdc1  37213  inxprnres  37758  fsumshftd  38418  pmapglb  39237  polval2N  39373  osumcllem4N  39426  pexmidlem1N  39437  dih1dimatlem  40796  mapdh9a  41256  mapdh9aOLDN  41257  sticksstones2  41613  selvvvval  41812  fsuppind  41817  elrab2w  42086  fphpd  42230  fphpdo  42231  pellex  42249  setindtrs  42440  dford3lem2  42442  fnwe2lem2  42469  mendlmod  42611  cantnfub  42744  tfsconcat0i  42768  rababg  42998  fsovrfovd  43433  fsovcnvlem  43437  scottabf  43671  elunif  44372  iunincfi  44454  cbvmpo2  44457  cbvmpo1  44458  disjf1  44550  wessf1ornlem  44552  disjinfi  44559  supxrleubrnmptf  44827  monoordxr  44859  monoord2xr  44861  fsummulc1f  44953  fsumnncl  44954  fsumf1of  44956  fsumiunss  44957  fsumreclf  44958  fsumlessf  44959  fsumsermpt  44961  fmulcl  44963  fmul01lt1lem2  44967  fprodexp  44976  fprodabs2  44977  climmulf  44986  climexp  44987  climrecf  44991  climinff  44993  climaddf  44997  mullimc  44998  limcperiod  45010  sumnnodd  45012  neglimc  45029  addlimc  45030  climsubmpt  45042  climreclf  45046  climeldmeqmpt  45050  climfveqmpt  45053  fnlimfvre  45056  climfveqf  45062  climfveqmpt3  45064  climeldmeqf  45065  climeqf  45070  climeldmeqmpt3  45071  climinf2  45089  limsupequz  45105  limsupequzmptf  45113  lmbr3  45129  cnrefiisp  45212  cncfshift  45256  fprodcncf  45282  dvmptmulf  45319  dvmptfprod  45327  dvnprodlem1  45328  dvnprodlem3  45330  stoweidlem16  45398  stoweidlem34  45416  stoweidlem62  45444  dirkercncflem2  45486  fourierdlem12  45501  fourierdlem15  45504  fourierdlem34  45523  fourierdlem50  45538  fourierdlem73  45561  fourierdlem94  45582  fourierdlem112  45600  fourierdlem113  45601  intsaluni  45711  sge0lempt  45792  sge0iunmptlemfi  45795  sge0iunmptlemre  45797  sge0iunmpt  45800  sge0ltfirpmpt2  45808  sge0isummpt2  45814  sge0xaddlem2  45816  sge0xadd  45817  meadjiun  45848  voliunsge0lem  45854  meaiuninclem  45862  meaiunincf  45865  meaiuninc3v  45866  meaiuninc3  45867  meaiininclem  45868  meaiininc  45869  isomennd  45913  ovn0lem  45947  sge0hsphoire  45971  hoidmvlelem1  45977  hoidmvlelem2  45978  hoidmvlelem3  45979  hoidmvlelem5  45981  hspmbllem2  46009  hoimbl2  46047  vonhoire  46054  vonioo  46064  vonicc  46067  vonn0ioo2  46072  vonn0icc2  46074  pimincfltioc  46098  salpreimagtlt  46112  smflimlem4  46156  rexrsb  46474  ichexmpl2  46804  ichnreuop  46806  sbgoldbm  47118  bgoldbnnsum3prm  47138  tgoldbach  47151  srhmsubcALTV  47381  cbvmpox2  47393  mo0sn  47880  f1omo  47907  isthincd2lem1  48027  thincmo  48029