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  3215  cbvralvw  3216  cbvrexvw  3217  cbvralfw  3278  cbvralsvw  3289  cbvralf  3323  ralcom2  3340  moel  3363  cbvrmovw  3364  cbvreuvw  3365  cbvrmow  3368  cbvreu  3382  cbvrabv  3400  rabrabi  3409  cbvrabw  3425  cbvrabwOLD  3426  nfrab  3428  cbvrab  3429  elrab2w  3639  reu2  3672  reu6  3673  rmo4  3677  reu8  3680  2reu5  3705  ruOLD  3728  csbied  3874  difjust  3892  unjust  3894  injust  3896  dfss2  3908  dfssf  3913  dfdif3OLD  4059  eqeuel  4306  rabeq0w  4328  disj  4391  reldisj  4394  ralidmw  4457  dfif6  4470  rabsnifsb  4667  eluniab  4865  unissb  4884  uniintsn  4928  dfiun2g  4973  dfiunv2  4977  disjxun  5084  cbvmptf  5186  cbvmptfg  5187  cbvmptv  5190  dftr2c  5196  isso2i  5570  dfres2  6001  imai  6034  frpoinsg  6302  tz7.7  6344  fvn0ssdmfun  7021  fmptco  7077  cbvriotaw  7327  cbvriotavw  7328  cbvriota  7331  cbvmpox  7454  cbvmpov  7456  tfis  7800  tfindes  7808  peano5  7838  findes  7845  dfoprab4f  8003  fmpox  8014  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  9603  cantnf  9608  setind  9662  frinsg  9669  tz9.12lem3  9707  infxpen  9930  dfac5lem4  10042  dfac12lem2  10061  kmlem14  10080  cfsmolem  10186  sornom  10193  isf32lem9  10277  axdc2  10365  fpwwe2lem7  10554  fpwwe2  10560  wunex2  10655  dedekindle  11304  wloglei  11676  uzind4s  12852  seqof2  14016  reuccatpfxs1  14703  shftfn  15029  rexuz3  15305  zsum  15674  fsum  15676  sumss  15680  sumss2  15682  fsumcvg2  15683  fsumser  15686  fsumclf  15694  fsumsplitf  15698  isumless  15804  prodfdiv  15855  cbvprod  15872  cbvprodv  15873  zprod  15896  fprod  15900  fprodntriv  15901  prodss  15906  fprod2dlem  15939  fproddivf  15946  fprodsplitf  15947  rpnnen2lem10  16184  cpnnen  16190  sumeven  16350  sumodd  16351  sadcp1  16418  smupp1  16443  pcmptdvds  16859  prmreclem2  16882  prmreclem5  16885  prmreclem6  16886  prmrec  16887  prmdvdsprmo  17007  iscatd2  17641  initoeu2  17977  yoniso  18245  sgrpidmnd  18701  mndind  18790  eqg0subg  19165  symggen  19439  dprd2d2  20015  srhmsubc  20651  isdrngrd  20737  isdrngrdOLD  20739  lbspss  21072  frlmphl  21774  frlmup1  21791  opsrtoslem1  22046  mdetralt  22586  mdetralt2  22587  mdetunilem2  22591  maducoeval2  22618  chfacfscmulgsum  22838  chfacfpmmulgsum  22842  isclo2  23066  neiptopnei  23110  ptcldmpt  23592  elmptrab  23805  hausflimi  23958  hausflim  23959  alexsubALTlem3  24027  alexsubALTlem4  24028  ptcmplem2  24031  cnextcn  24045  cnextfres1  24046  tgphaus  24095  ustuqtop  24224  utopsnneip  24226  ucncn  24262  nrmmetd  24552  xrhmeo  24926  iscau2  25257  caucfil  25263  cmetcaulem  25268  bcth  25309  vitalilem3  25590  vitali  25593  i1f1lem  25669  itg11  25671  i1fres  25685  mbfi1fseq  25701  mbfi1flim  25703  itg2uba  25723  itg2splitlem  25728  isibl2  25746  cbvitg  25756  cbvitgv  25757  itgss3  25795  dvmptfsum  25955  rolle  25970  elply2  26174  plyexmo  26293  lgamgulmlem2  27010  prmorcht  27158  pclogsum  27195  dchr1  27237  lgsdir  27312  lgsdilem2  27313  lgsdi  27314  lgsne0  27315  lgsquadlem3  27362  lgsquad  27363  2sqlem8  27406  nosupcbv  27683  nosupno  27684  nosupdm  27685  nosupbnd1lem1  27689  noinfcbv  27698  noinfno  27699  noinfdm  27700  nocvxminlem  27763  legval  28669  legov  28670  tglineintmo  28727  tglowdim2ln  28736  ishpg  28844  lnopp2hpgb  28848  hpgerlem  28850  colopp  28854  axcontlem1  29050  numedglnl  29230  uvtxnbgrvtx  29479  cusgrres  29535  wspniunwspnon  30009  rusgrnumwwlkb0  30060  frgr3vlem2  30362  3vfriswmgrlem  30365  fusgr2wsp2nb  30422  numclwlk2lem2f1o  30467  lpni  30569  pjhthmo  31391  chscllem2  31727  cbvdisjf  32659  2ndresdju  32740  fmptcof2  32748  aciunf1lem  32753  funcnv4mpt  32759  suppovss  32772  fpwrelmapffslem  32823  fsumiunle  32920  gsumwrd2dccatlem  33156  elrspunsn  33507  1arithufdlem3  33624  fedgmullem1  33792  fldextrspunlsp  33837  extdgfialglem2  33856  zarclssn  34036  esumcvg  34249  fiunelros  34337  measiun  34381  bnj1146  34952  bnj1185  34954  bnj1385  34993  bnj1014  35122  bnj1112  35144  bnj1123  35147  bnj1228  35172  bnj1326  35187  bnj1321  35188  bnj1384  35193  bnj1417  35202  bnj1497  35221  trssfir1om  35274  r1omhfb  35275  fineqvnttrclse  35287  axregscl  35291  setindregs  35293  trssfir1omregs  35299  r1omhfbregs  35300  onvf1odlem2  35305  onvf1odlem3  35306  gonarlem  35595  goalrlem  35597  goalr  35598  mrsubrn  35714  dfon2lem6  35987  dfbigcup2  36098  lineintmo  36358  cbvralvw2  36427  cbvrexvw2  36428  cbvrmovw2  36429  cbvreuvw2  36430  cbvmptvw2  36435  cbvprodvw2  36448  cbvrmodavw  36453  cbvreudavw  36454  cbvrabdavw  36462  cbvmptdavw  36468  cbvriotadavw  36471  cbvixpdavw  36479  cbvproddavw  36481  cbvitgdavw  36482  cbvrabdavw2  36486  cbvmptdavw2  36489  cbvriotadavw2  36491  weiunlem  36664  dfttc4  36731  mh-infprim2bi  36748  eleq2w2ALT  37373  bj-idres  37493  mptsnunlem  37671  wl-dfcleq  37847  wl-dfclel  37848  ptrest  37957  poimirlem25  37983  mblfinlem2  37996  mblfinlem3  37997  mblfinlem4  37998  ismblfin  37999  mbfposadd  38005  itg2addnclem  38009  ftc1anclem5  38035  ftc1anclem6  38036  ftc1anclem7  38037  ftc1anc  38039  areacirclem5  38050  fdc1  38084  inxprnres  38636  fsumshftd  39415  pmapglb  40233  polval2N  40369  osumcllem4N  40422  pexmidlem1N  40433  dih1dimatlem  41792  mapdh9a  42252  mapdh9aOLDN  42253  sticksstones2  42603  selvvvval  43035  fsuppind  43040  fphpd  43265  fphpdo  43266  pellex  43284  setindtrs  43474  dford3lem2  43476  fnwe2lem2  43500  mendlmod  43638  cantnfub  43770  tfsconcat0i  43794  rababg  44022  fsovrfovd  44457  fsovcnvlem  44461  scottabf  44688  trfr  45410  elunif  45468  iunincfi  45545  cbvmpo2  45548  cbvmpo1  45549  disjf1  45634  wessf1ornlem  45636  disjinfi  45643  supxrleubrnmptf  45900  monoordxr  45931  monoord2xr  45933  fsummulc1f  46022  fsumnncl  46023  fsumf1of  46025  fsumiunss  46026  fsumreclf  46027  fsumlessf  46028  fsumsermpt  46030  fmulcl  46032  fmul01lt1lem2  46036  fprodexp  46045  fprodabs2  46046  climmulf  46055  climexp  46056  climrecf  46060  climinff  46062  climaddf  46066  mullimc  46067  limcperiod  46079  sumnnodd  46081  neglimc  46096  addlimc  46097  climsubmpt  46109  climreclf  46113  climeldmeqmpt  46117  climfveqmpt  46120  fnlimfvre  46123  climfveqf  46129  climfveqmpt3  46131  climeldmeqf  46132  climeqf  46137  climeldmeqmpt3  46138  climinf2  46156  limsupequz  46172  limsupequzmptf  46180  lmbr3  46196  cnrefiisp  46279  cncfshift  46323  fprodcncf  46349  dvmptmulf  46386  dvmptfprod  46394  dvnprodlem1  46395  dvnprodlem3  46397  stoweidlem16  46465  stoweidlem34  46483  stoweidlem62  46511  dirkercncflem2  46553  fourierdlem12  46568  fourierdlem15  46571  fourierdlem34  46590  fourierdlem50  46605  fourierdlem73  46628  fourierdlem94  46649  fourierdlem112  46667  fourierdlem113  46668  intsaluni  46778  sge0lempt  46859  sge0iunmptlemfi  46862  sge0iunmptlemre  46864  sge0iunmpt  46867  sge0ltfirpmpt2  46875  sge0isummpt2  46881  sge0xaddlem2  46883  sge0xadd  46884  meadjiun  46915  voliunsge0lem  46921  meaiuninclem  46929  meaiunincf  46932  meaiuninc3v  46933  meaiuninc3  46934  meaiininclem  46935  meaiininc  46936  isomennd  46980  ovn0lem  47014  sge0hsphoire  47038  hoidmvlelem1  47044  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem5  47048  hspmbllem2  47076  hoimbl2  47114  vonhoire  47121  vonioo  47131  vonicc  47134  vonn0ioo2  47139  vonn0icc2  47141  pimincfltioc  47165  salpreimagtlt  47179  smflimlem4  47223  ormkglobd  47324  sinnpoly  47354  rexrsb  47563  ichexmpl2  47945  ichnreuop  47947  sbgoldbm  48275  bgoldbnnsum3prm  48295  tgoldbach  48308  srhmsubcALTV  48816  cbvmpox2  48827  mo0sn  49306  f1omoOLD  49384  isthincd2lem1  49915  thincmo  49918  euendfunc  50016