Theorem eleq1w 2895

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

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∃wex 1780   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-clel 2893

This theorem is referenced by:  cleqh  2936  clelsb3  2940  clelsb3vOLD  2941  nfcjust  2962  clelsb3fOLD  2983  cleqf  3010  ralcom2  3363  nfrab  3386  cbvralfw  3437  cbvralf  3439  cbvreuw  3443  cbvreu  3447  cbvralvw  3449  cbvrexvw  3450  cbvrabw  3489  cbvrab  3490  cbvrabv  3491  ralab2OLD  3689  rexab2OLD  3692  reu2  3716  reu6  3717  rmo4  3721  reu8  3724  2reu5  3749  ru  3771  difjust  3938  unjust  3940  injust  3942  dfss2f  3958  dfdif3  4091  eqeuel  4322  rabsnifsb  4658  eluniab  4853  elintab  4887  uniintsn  4913  dfiunv2  4960  disjxun  5064  cbvmptf  5165  cbvmptfg  5166  isso2i  5508  dfres2  5909  imai  5942  wfisg  6183  tz7.7  6217  fvn0ssdmfun  6842  fmptco  6891  cbvriotaw  7123  cbvriota  7127  cbvmpox  7247  tfis  7569  tfindes  7577  findes  7612  dfoprab4f  7754  fmpox  7765  wfrlem10  7964  smogt  8004  resixpfo  8500  ixpsnf1o  8502  dom2lem  8549  mapsnend  8588  pw2f1olem  8621  findcard3  8761  ordiso2  8979  elirrv  9060  cantnflem1d  9151  cantnf  9156  setind  9176  tz9.12lem3  9218  infxpen  9440  dfac12lem2  9570  kmlem14  9589  cfsmolem  9692  sornom  9699  isf32lem9  9783  axdc2  9871  fpwwe2lem8  10059  fpwwe2  10065  wunex2  10160  dedekindle  10804  wloglei  11172  uzind4s  12309  seqof2  13429  reuccatpfxs1  14109  shftfn  14432  rexuz3  14708  zsum  15075  fsum  15077  sumss  15081  sumss2  15083  fsumcvg2  15084  fsumser  15087  fsumsplitf  15098  isumless  15200  prodfdiv  15252  cbvprod  15269  zprod  15291  fprod  15295  fprodntriv  15296  prodss  15301  fprod2dlem  15334  fproddivf  15341  fprodsplitf  15342  rpnnen2lem10  15576  cpnnen  15582  sumeven  15738  sumodd  15739  sadcp1  15804  smupp1  15829  pcmptdvds  16230  prmreclem2  16253  prmreclem5  16256  prmreclem6  16257  prmrec  16258  prmdvdsprmo  16378  iscatd2  16952  initoeu2  17276  yoniso  17535  sgrpidmnd  17916  mndind  17992  symggen  18598  dprd2d2  19166  isdrngrd  19528  lbspss  19854  opsrtoslem1  20264  frlmphl  20925  frlmup1  20942  mdetralt  21217  mdetralt2  21218  mdetunilem2  21222  maducoeval2  21249  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  isclo2  21696  neiptopnei  21740  ptcldmpt  22222  elmptrab  22435  hausflimi  22588  hausflim  22589  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem2  22661  cnextcn  22675  cnextfres1  22676  tgphaus  22725  ustuqtop  22855  utopsnneip  22857  ucncn  22894  nrmmetd  23184  xrhmeo  23550  iscau2  23880  caucfil  23886  cmetcaulem  23891  bcth  23932  vitalilem3  24211  vitali  24214  i1f1lem  24290  itg11  24292  i1fres  24306  mbfi1fseq  24322  mbfi1flim  24324  itg2uba  24344  itg2splitlem  24349  isibl2  24367  cbvitg  24376  itgss3  24415  dvmptfsum  24572  rolle  24587  elply2  24786  plyexmo  24902  lgamgulmlem2  25607  prmorcht  25755  pclogsum  25791  dchr1  25833  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  lgsquadlem3  25958  lgsquad  25959  2sqlem8  26002  legval  26370  legov  26371  tglineintmo  26428  tglowdim2ln  26437  ishpg  26545  lnopp2hpgb  26549  hpgerlem  26551  colopp  26555  axcontlem1  26750  numedglnl  26929  uvtxnbgrvtx  27175  cusgrres  27230  wspniunwspnon  27702  rusgrnumwwlkb0  27750  frgr3vlem2  28053  3vfriswmgrlem  28056  fusgr2wsp2nb  28113  numclwlk2lem2f1o  28158  lpni  28257  pjhthmo  29079  chscllem2  29415  moel  30252  cbvdisjf  30321  fmptcof2  30402  aciunf1lem  30407  funcnv4mpt  30414  suppovss  30426  fpwrelmapffslem  30468  fsumiunle  30545  fedgmullem1  31025  esumcvg  31345  fiunelros  31433  measiun  31477  bnj1146  32063  bnj1185  32065  bnj1385  32104  bnj1014  32233  bnj1112  32255  bnj1123  32258  bnj1228  32283  bnj1326  32298  bnj1321  32299  bnj1384  32304  bnj1417  32313  bnj1497  32332  gonarlem  32641  goalrlem  32643  goalr  32644  mrsubrn  32760  dfon2lem6  33033  frpoinsg  33081  frinsg  33087  poseq  33095  soseq  33096  nosupno  33203  nosupdm  33204  nosupbnd1lem1  33208  noeta  33222  nocvxminlem  33247  dfbigcup2  33360  lineintmo  33618  bj-idres  34455  mptsnunlem  34622  wl-dfralflem  34853  ptrest  34906  poimirlem25  34932  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  mbfposadd  34954  itg2addnclem  34958  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anc  34990  areacirclem5  35001  fdc1  35036  inxprnres  35564  fsumshftd  36103  pmapglb  36921  polval2N  37057  osumcllem4N  37110  pexmidlem1N  37121  dih1dimatlem  38480  mapdh9a  38940  mapdh9aOLDN  38941  fphpd  39433  fphpdo  39434  pellex  39452  setindtrs  39642  dford3lem2  39644  fnwe2lem2  39671  mendlmod  39813  rababg  39953  fsovrfovd  40375  fsovcnvlem  40379  scottabf  40596  elunif  41293  iunincfi  41380  cbvmpo2  41383  cbvmpo1  41384  disjf1  41463  wessf1ornlem  41465  disjinfi  41474  supxrleubrnmptf  41747  monoordxr  41779  monoord2xr  41781  fsumclf  41870  fsummulc1f  41871  fsumnncl  41872  fsumf1of  41875  fsumiunss  41876  fsumreclf  41877  fsumlessf  41878  fsumsermpt  41880  fmulcl  41882  fmul01lt1lem2  41886  fprodexp  41895  fprodabs2  41896  climmulf  41905  climexp  41906  climrecf  41910  climinff  41912  climaddf  41916  mullimc  41917  limcperiod  41929  sumnnodd  41931  neglimc  41948  addlimc  41949  climsubmpt  41961  climreclf  41965  climeldmeqmpt  41969  climfveqmpt  41972  fnlimfvre  41975  climfveqf  41981  climfveqmpt3  41983  climeldmeqf  41984  climeqf  41989  climeldmeqmpt3  41990  climinf2  42008  limsupequz  42024  limsupequzmptf  42032  lmbr3  42048  cnrefiisp  42131  cncfshift  42177  fprodcncf  42204  dvmptmulf  42242  dvmptfprod  42250  dvnprodlem1  42251  dvnprodlem3  42253  stoweidlem16  42321  stoweidlem34  42339  stoweidlem62  42367  dirkercncflem2  42409  fourierdlem12  42424  fourierdlem15  42427  fourierdlem34  42446  fourierdlem50  42461  fourierdlem73  42484  fourierdlem94  42505  fourierdlem112  42523  fourierdlem113  42524  intsaluni  42632  sge0lempt  42712  sge0iunmptlemfi  42715  sge0iunmptlemre  42717  sge0iunmpt  42720  sge0ltfirpmpt2  42728  sge0isummpt2  42734  sge0xaddlem2  42736  sge0xadd  42737  meadjiun  42768  voliunsge0lem  42774  meaiuninclem  42782  meaiunincf  42785  meaiuninc3v  42786  meaiuninc3  42787  meaiininclem  42788  meaiininc  42789  isomennd  42833  ovn0lem  42867  sge0hsphoire  42891  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem5  42901  hspmbllem2  42929  hoimbl2  42967  vonhoire  42974  vonioo  42984  vonicc  42987  vonn0ioo2  42992  vonn0icc2  42994  pimincfltioc  43014  salpreimagtlt  43027  smflimlem4  43070  rexrsb  43318  ichexmpl2  43652  ichnreuop  43654  sbgoldbm  43969  bgoldbnnsum3prm  43989  tgoldbach  44002  srhmsubc  44367  srhmsubcALTV  44385  cbvmpox2  44404