Theorem eleq1w 2895

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

Note that this provides a proof of ax-8 2112 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 2029	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1918	. 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 1776   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  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  3688  rexab2OLD  3691  reu2  3715  reu6  3716  rmo4  3720  reu8  3723  2reu5  3748  ru  3770  difjust  3937  unjust  3939  injust  3941  dfss2f  3957  dfdif3  4090  eqeuel  4321  rabsnifsb  4651  eluniab  4842  elintab  4879  uniintsn  4905  dfiunv2  4952  disjxun  5056  cbvmptf  5157  cbvmptfg  5158  isso2i  5502  dfres2  5903  imai  5936  wfisg  6177  tz7.7  6211  fvn0ssdmfun  6836  fmptco  6885  cbvriotaw  7117  cbvriota  7121  cbvmpox  7241  tfis  7563  tfindes  7571  findes  7606  dfoprab4f  7748  fmpox  7759  wfrlem10  7958  smogt  7998  resixpfo  8494  ixpsnf1o  8496  dom2lem  8543  mapsnend  8582  pw2f1olem  8615  findcard3  8755  ordiso2  8973  elirrv  9054  cantnflem1d  9145  cantnf  9150  setind  9170  tz9.12lem3  9212  infxpen  9434  dfac12lem2  9564  kmlem14  9583  cfsmolem  9686  sornom  9693  isf32lem9  9777  axdc2  9865  fpwwe2lem8  10053  fpwwe2  10059  wunex2  10154  dedekindle  10798  wloglei  11166  uzind4s  12302  seqof2  13422  reuccatpfxs1  14103  shftfn  14426  rexuz3  14702  zsum  15069  fsum  15071  sumss  15075  sumss2  15077  fsumcvg2  15078  fsumser  15081  fsumsplitf  15092  isumless  15194  prodfdiv  15246  cbvprod  15263  zprod  15285  fprod  15289  fprodntriv  15290  prodss  15295  fprod2dlem  15328  fproddivf  15335  fprodsplitf  15336  rpnnen2lem10  15570  cpnnen  15576  sumeven  15732  sumodd  15733  sadcp1  15798  smupp1  15823  pcmptdvds  16224  prmreclem2  16247  prmreclem5  16250  prmreclem6  16251  prmrec  16252  prmdvdsprmo  16372  iscatd2  16946  initoeu2  17270  yoniso  17529  sgrpidmnd  17910  mndind  17986  symggen  18592  dprd2d2  19160  isdrngrd  19522  lbspss  19848  opsrtoslem1  20258  frlmphl  20919  frlmup1  20936  mdetralt  21211  mdetralt2  21212  mdetunilem2  21216  maducoeval2  21243  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  isclo2  21690  neiptopnei  21734  ptcldmpt  22216  elmptrab  22429  hausflimi  22582  hausflim  22583  alexsubALTlem3  22651  alexsubALTlem4  22652  ptcmplem2  22655  cnextcn  22669  cnextfres1  22670  tgphaus  22719  ustuqtop  22849  utopsnneip  22851  ucncn  22888  nrmmetd  23178  xrhmeo  23544  iscau2  23874  caucfil  23880  cmetcaulem  23885  bcth  23926  vitalilem3  24205  vitali  24208  i1f1lem  24284  itg11  24286  i1fres  24300  mbfi1fseq  24316  mbfi1flim  24318  itg2uba  24338  itg2splitlem  24343  isibl2  24361  cbvitg  24370  itgss3  24409  dvmptfsum  24566  rolle  24581  elply2  24780  plyexmo  24896  lgamgulmlem2  25601  prmorcht  25749  pclogsum  25785  dchr1  25827  lgsdir  25902  lgsdilem2  25903  lgsdi  25904  lgsne0  25905  lgsquadlem3  25952  lgsquad  25953  2sqlem8  25996  legval  26364  legov  26365  tglineintmo  26422  tglowdim2ln  26431  ishpg  26539  lnopp2hpgb  26543  hpgerlem  26545  colopp  26549  axcontlem1  26744  numedglnl  26923  uvtxnbgrvtx  27169  cusgrres  27224  wspniunwspnon  27696  rusgrnumwwlkb0  27744  frgr3vlem2  28047  3vfriswmgrlem  28050  fusgr2wsp2nb  28107  numclwlk2lem2f1o  28152  lpni  28251  pjhthmo  29073  chscllem2  29409  moel  30246  cbvdisjf  30315  fmptcof2  30396  aciunf1lem  30401  funcnv4mpt  30408  suppovss  30420  fpwrelmapffslem  30462  fsumiunle  30540  fedgmullem1  31020  esumcvg  31340  fiunelros  31428  measiun  31472  bnj1146  32058  bnj1185  32060  bnj1385  32099  bnj1014  32228  bnj1112  32250  bnj1123  32253  bnj1228  32278  bnj1326  32293  bnj1321  32294  bnj1384  32299  bnj1417  32308  bnj1497  32327  gonarlem  32636  goalrlem  32638  goalr  32639  mrsubrn  32755  dfon2lem6  33028  frpoinsg  33076  frinsg  33082  poseq  33090  soseq  33091  nosupno  33198  nosupdm  33199  nosupbnd1lem1  33203  noeta  33217  nocvxminlem  33242  dfbigcup2  33355  lineintmo  33613  bj-idres  34446  mptsnunlem  34613  wl-dfralflem  34832  ptrest  34885  poimirlem25  34911  mblfinlem2  34924  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  mbfposadd  34933  itg2addnclem  34937  ftc1anclem5  34965  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anc  34969  areacirclem5  34980  fdc1  35015  inxprnres  35543  fsumshftd  36082  pmapglb  36900  polval2N  37036  osumcllem4N  37089  pexmidlem1N  37100  dih1dimatlem  38459  mapdh9a  38919  mapdh9aOLDN  38920  fphpd  39406  fphpdo  39407  pellex  39425  setindtrs  39615  dford3lem2  39617  fnwe2lem2  39644  mendlmod  39786  rababg  39926  fsovrfovd  40348  fsovcnvlem  40352  scottabf  40569  elunif  41266  iunincfi  41353  cbvmpo2  41356  cbvmpo1  41357  disjf1  41436  wessf1ornlem  41438  disjinfi  41447  supxrleubrnmptf  41720  monoordxr  41752  monoord2xr  41754  fsumclf  41843  fsummulc1f  41844  fsumnncl  41845  fsumf1of  41848  fsumiunss  41849  fsumreclf  41850  fsumlessf  41851  fsumsermpt  41853  fmulcl  41855  fmul01lt1lem2  41859  fprodexp  41868  fprodabs2  41869  climmulf  41878  climexp  41879  climrecf  41883  climinff  41885  climaddf  41889  mullimc  41890  limcperiod  41902  sumnnodd  41904  neglimc  41921  addlimc  41922  climsubmpt  41934  climreclf  41938  climeldmeqmpt  41942  climfveqmpt  41945  fnlimfvre  41948  climfveqf  41954  climfveqmpt3  41956  climeldmeqf  41957  climeqf  41962  climeldmeqmpt3  41963  climinf2  41981  limsupequz  41997  limsupequzmptf  42005  lmbr3  42021  cnrefiisp  42104  cncfshift  42150  fprodcncf  42177  dvmptmulf  42215  dvmptfprod  42223  dvnprodlem1  42224  dvnprodlem3  42226  stoweidlem16  42295  stoweidlem34  42313  stoweidlem62  42341  dirkercncflem2  42383  fourierdlem12  42398  fourierdlem15  42401  fourierdlem34  42420  fourierdlem50  42435  fourierdlem73  42458  fourierdlem94  42479  fourierdlem112  42497  fourierdlem113  42498  intsaluni  42606  sge0lempt  42686  sge0iunmptlemfi  42689  sge0iunmptlemre  42691  sge0iunmpt  42694  sge0ltfirpmpt2  42702  sge0isummpt2  42708  sge0xaddlem2  42710  sge0xadd  42711  meadjiun  42742  voliunsge0lem  42748  meaiuninclem  42756  meaiunincf  42759  meaiuninc3v  42760  meaiuninc3  42761  meaiininclem  42762  meaiininc  42763  isomennd  42807  ovn0lem  42841  sge0hsphoire  42865  hoidmvlelem1  42871  hoidmvlelem2  42872  hoidmvlelem3  42873  hoidmvlelem5  42875  hspmbllem2  42903  hoimbl2  42941  vonhoire  42948  vonioo  42958  vonicc  42961  vonn0ioo2  42966  vonn0icc2  42968  pimincfltioc  42988  salpreimagtlt  43001  smflimlem4  43044  rexrsb  43292  ichexmpl2  43626  ichnreuop  43628  sbgoldbm  43943  bgoldbnnsum3prm  43963  tgoldbach  43976  srhmsubc  44341  srhmsubcALTV  44359  cbvmpox2  44378