Theorem eleq1w 2822

Description: Weaker version of eleq1 2827 (but more general than elequ1 2114) not depending on ax-ext 2710 nor df-cleq 2731.

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃wex 1782   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2817

This theorem is referenced by:  cleqh  2863  clelsb1  2867  nfcjust  2889  nfcr  2893  nfcriOLD  2898  nfcriOLDOLD  2899  cleqf  2939  rspw  3131  ralcom2  3291  nfrab  3321  moel  3359  moelOLD  3360  cbvralfw  3369  cbvralfwOLD  3370  cbvralf  3372  cbvrmow  3376  cbvreuwOLD  3378  cbvreu  3382  cbvralvw  3384  cbvrexvw  3385  cbvrmovw  3386  cbvreuvw  3387  cbvrabw  3425  cbvrab  3426  cbvrabv  3427  rabrabi  3428  reu2  3661  reu6  3662  rmo4  3666  reu8  3669  2reu5  3694  ru  3716  csbied  3871  difjust  3890  unjust  3892  injust  3894  dfss2f  3912  dfdif3  4050  eqeuel  4297  rabeq0w  4318  disj  4382  reldisj  4386  ralidmw  4439  dfif6  4463  rabsnifsb  4659  eluniab  4855  elintab  4891  uniintsn  4919  dfiun2g  4961  dfiunv2  4966  disjxun  5073  cbvmptf  5184  cbvmptfg  5185  cbvmptv  5188  isso2i  5539  dfres2  5952  imai  5985  frpoinsg  6250  wfisgOLD  6261  tz7.7  6296  fvn0ssdmfun  6961  fmptco  7010  cbvriotaw  7250  cbvriotavw  7251  cbvriota  7255  cbvmpox  7377  tfis  7710  tfindes  7718  peano5  7749  findes  7758  dfoprab4f  7905  fmpox  7916  wfrlem10OLD  8158  smogt  8207  resixpfo  8733  ixpsnf1o  8735  dom2lem  8789  mapsnend  8835  pw2f1olem  8872  pssnn  8960  ssfi  8965  findcard3  9066  ordiso2  9283  elirrv  9364  cantnflem1d  9455  cantnf  9460  setind  9501  frinsg  9518  tz9.12lem3  9556  infxpen  9779  dfac12lem2  9909  kmlem14  9928  cfsmolem  10035  sornom  10042  isf32lem9  10126  axdc2  10214  fpwwe2lem7  10402  fpwwe2  10408  wunex2  10503  dedekindle  11148  wloglei  11516  uzind4s  12657  seqof2  13790  reuccatpfxs1  14469  shftfn  14793  rexuz3  15069  zsum  15439  fsum  15441  sumss  15445  sumss2  15447  fsumcvg2  15448  fsumser  15451  fsumclf  15459  fsumsplitf  15463  isumless  15566  prodfdiv  15617  cbvprod  15634  zprod  15656  fprod  15660  fprodntriv  15661  prodss  15666  fprod2dlem  15699  fproddivf  15706  fprodsplitf  15707  rpnnen2lem10  15941  cpnnen  15947  sumeven  16105  sumodd  16106  sadcp1  16171  smupp1  16196  pcmptdvds  16604  prmreclem2  16627  prmreclem5  16630  prmreclem6  16631  prmrec  16632  prmdvdsprmo  16752  iscatd2  17399  initoeu2  17740  yoniso  18012  sgrpidmnd  18399  mndind  18475  symggen  19087  dprd2d2  19656  isdrngrd  20026  lbspss  20353  frlmphl  20997  frlmup1  21014  opsrtoslem1  21271  mdetralt  21766  mdetralt2  21767  mdetunilem2  21771  maducoeval2  21798  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  isclo2  22248  neiptopnei  22292  ptcldmpt  22774  elmptrab  22987  hausflimi  23140  hausflim  23141  alexsubALTlem3  23209  alexsubALTlem4  23210  ptcmplem2  23213  cnextcn  23227  cnextfres1  23228  tgphaus  23277  ustuqtop  23407  utopsnneip  23409  ucncn  23446  nrmmetd  23739  xrhmeo  24118  iscau2  24450  caucfil  24456  cmetcaulem  24461  bcth  24502  vitalilem3  24783  vitali  24786  i1f1lem  24862  itg11  24864  i1fres  24879  mbfi1fseq  24895  mbfi1flim  24897  itg2uba  24917  itg2splitlem  24922  isibl2  24940  cbvitg  24949  itgss3  24988  dvmptfsum  25148  rolle  25163  elply2  25366  plyexmo  25482  lgamgulmlem2  26188  prmorcht  26336  pclogsum  26372  dchr1  26414  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  lgsquadlem3  26539  lgsquad  26540  2sqlem8  26583  legval  26954  legov  26955  tglineintmo  27012  tglowdim2ln  27021  ishpg  27129  lnopp2hpgb  27133  hpgerlem  27135  colopp  27139  axcontlem1  27341  numedglnl  27523  uvtxnbgrvtx  27769  cusgrres  27824  wspniunwspnon  28297  rusgrnumwwlkb0  28345  frgr3vlem2  28647  3vfriswmgrlem  28650  fusgr2wsp2nb  28707  numclwlk2lem2f1o  28752  lpni  28851  pjhthmo  29673  chscllem2  30009  cbvdisjf  30919  2ndresdju  30995  fmptcof2  31003  aciunf1lem  31008  funcnv4mpt  31015  suppovss  31026  fpwrelmapffslem  31076  fsumiunle  31152  fedgmullem1  31719  zarclssn  31832  esumcvg  32063  fiunelros  32151  measiun  32195  bnj1146  32780  bnj1185  32782  bnj1385  32821  bnj1014  32950  bnj1112  32972  bnj1123  32975  bnj1228  33000  bnj1326  33015  bnj1321  33016  bnj1384  33021  bnj1417  33030  bnj1497  33049  gonarlem  33365  goalrlem  33367  goalr  33368  mrsubrn  33484  dfon2lem6  33773  xpord2ind  33803  xpord3ind  33809  poseq  33811  soseq  33812  nosupcbv  33914  nosupno  33915  nosupdm  33916  nosupbnd1lem1  33920  noinfcbv  33929  noinfno  33930  noinfdm  33931  nocvxminlem  33981  dfbigcup2  34210  lineintmo  34468  eleq2w2ALT  35229  bj-idres  35340  mptsnunlem  35518  ptrest  35785  poimirlem25  35811  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  mbfposadd  35833  itg2addnclem  35837  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anc  35867  areacirclem5  35878  fdc1  35913  inxprnres  36435  fsumshftd  36973  pmapglb  37791  polval2N  37927  osumcllem4N  37980  pexmidlem1N  37991  dih1dimatlem  39350  mapdh9a  39810  mapdh9aOLDN  39811  sticksstones2  40110  elrab2w  40174  fsuppind  40286  fphpd  40645  fphpdo  40646  pellex  40664  setindtrs  40854  dford3lem2  40856  fnwe2lem2  40883  mendlmod  41025  rababg  41188  fsovrfovd  41624  fsovcnvlem  41628  scottabf  41865  elunif  42566  iunincfi  42651  cbvmpo2  42654  cbvmpo1  42655  disjf1  42727  wessf1ornlem  42729  disjinfi  42738  supxrleubrnmptf  42998  monoordxr  43030  monoord2xr  43032  fsummulc1f  43119  fsumnncl  43120  fsumf1of  43122  fsumiunss  43123  fsumreclf  43124  fsumlessf  43125  fsumsermpt  43127  fmulcl  43129  fmul01lt1lem2  43133  fprodexp  43142  fprodabs2  43143  climmulf  43152  climexp  43153  climrecf  43157  climinff  43159  climaddf  43163  mullimc  43164  limcperiod  43176  sumnnodd  43178  neglimc  43195  addlimc  43196  climsubmpt  43208  climreclf  43212  climeldmeqmpt  43216  climfveqmpt  43219  fnlimfvre  43222  climfveqf  43228  climfveqmpt3  43230  climeldmeqf  43231  climeqf  43236  climeldmeqmpt3  43237  climinf2  43255  limsupequz  43271  limsupequzmptf  43279  lmbr3  43295  cnrefiisp  43378  cncfshift  43422  fprodcncf  43448  dvmptmulf  43485  dvmptfprod  43493  dvnprodlem1  43494  dvnprodlem3  43496  stoweidlem16  43564  stoweidlem34  43582  stoweidlem62  43610  dirkercncflem2  43652  fourierdlem12  43667  fourierdlem15  43670  fourierdlem34  43689  fourierdlem50  43704  fourierdlem73  43727  fourierdlem94  43748  fourierdlem112  43766  fourierdlem113  43767  intsaluni  43875  sge0lempt  43955  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0iunmpt  43963  sge0ltfirpmpt2  43971  sge0isummpt2  43977  sge0xaddlem2  43979  sge0xadd  43980  meadjiun  44011  voliunsge0lem  44017  meaiuninclem  44025  meaiunincf  44028  meaiuninc3v  44029  meaiuninc3  44030  meaiininclem  44031  meaiininc  44032  isomennd  44076  ovn0lem  44110  sge0hsphoire  44134  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem5  44144  hspmbllem2  44172  hoimbl2  44210  vonhoire  44217  vonioo  44227  vonicc  44230  vonn0ioo2  44235  vonn0icc2  44237  pimincfltioc  44261  salpreimagtlt  44275  smflimlem4  44319  rexrsb  44603  ichexmpl2  44933  ichnreuop  44935  sbgoldbm  45247  bgoldbnnsum3prm  45267  tgoldbach  45280  srhmsubc  45645  srhmsubcALTV  45663  cbvmpox2  45682  mo0sn  46172  f1omo  46199  isthincd2lem1  46319  thincmo  46321