Theorem eleq1w 2843

Description: Weaker version of eleq1 2848 (but more general than elequ1 2152) not depending on ax-ext 2732 nor df-cleq 2752.

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2835

This theorem is used by:  clelsb1  2887  cleqh  2889  nfcjust  2908  nfcr  2912  cleqf  2950  rspw  3239  cbvralvw  3240  cbvrexvw  3241  cbvralfw  3302  cbvralsvw  3313  cbvralf  3345  ralcom2  3362  moel  3385  cbvrmovw  3386  cbvreuvw  3387  cbvrmow  3390  cbvreu  3404  cbvrabv  3422  rabrabi  3430  cbvrabw  3446  nfrab  3448  cbvrab  3449  elrab2w  3650  reu2  3683  reu6  3684  rmo4  3688  reu8  3691  2reu5  3716  csbied  3883  difjust  3901  unjust  3903  injust  3905  dfss2  3917  dfssf  3922  eqeuel  4313  rabeq0w  4337  disj  4403  reldisj  4406  ralidmw  4472  dfif6  4485  rabsnifsb  4683  eluniab  4881  unissb  4901  uniintsn  4945  dfiun2g  4988  dfiunv2  4992  disjxun  5101  cbvmptf  5205  cbvmptfg  5206  cbvmptv  5209  dftr2c  5215  isso2i  5600  dfres2  6037  imai  6070  frpoinsg  6341  tz7.7  6383  fvn0ssdmfun  7068  fmptco  7124  cbvriotaw  7380  cbvriotavw  7381  cbvriota  7384  cbvmpox  7507  cbvmpov  7509  tfis  7852  tfindes  7860  peano5  7891  findes  7898  dfoprab4f  8054  fmpox  8065  xpord2indlem  8146  poseq  8157  soseq  8158  smogt  8357  resixpfo  8944  ixpsnf1o  8946  dom2lem  8999  mapsnend  9044  pw2f1olem  9080  pssnn  9164  ssfi  9168  findcard3  9254  ordiso2  9488  elirrvOLDOLD  9572  cantnflem1d  9668  cantnf  9673  setind  9727  frinsg  9734  tz9.12lem3  9772  scottabf  9879  infxpen  10018  dfac5lem4  10130  dfac12lem2  10148  kmlem14  10167  cfsmolem  10273  sornom  10280  isf32lem9  10364  axdc2  10452  fpwwe2lem7  10647  fpwwe2  10653  wunex2  10748  dedekindle  11399  wloglei  11771  uzind4s  12958  seqof2  14125  reuccatpfxs1  14817  shftfn  15147  rexuz3  15437  zsum  15805  fsum  15807  sumss  15811  sumss2  15813  fsumcvg2  15814  fsumser  15817  fsumclf  15825  fsumsplitf  15829  isumless  15935  prodfdiv  15986  cbvprod  16003  cbvprodv  16004  zprod  16025  fprod  16029  fprodntriv  16030  prodss  16035  fprod2dlem  16068  fproddivf  16075  fprodsplitf  16076  rpnnen2lem10  16312  cpnnen  16318  sumeven  16478  sumodd  16479  sadcp1  16546  smupp1  16571  pcmptdvds  16987  prmreclem2  17010  prmreclem5  17013  prmreclem6  17014  prmrec  17015  prmdvdsprmo  17135  iscatd2  17770  initoeu2  18106  yoniso  18374  sgrpidmnd  18842  mndind  18938  eqg0subg  19325  symggen  19598  dprd2d2  20174  srhmsubc  20843  isdrngrd  20933  isdrngrdOLD  20935  lbspss  21267  frlmphl  21995  frlmup1  22012  opsrtoslem1  22272  selvvvval  22359  mdetralt  22831  mdetralt2  22832  mdetunilem2  22836  maducoeval2  22863  chfacfscmulgsum  23086  chfacfpmmulgsum  23090  isclo2  23314  neiptopnei  23358  ptcldmpt  23841  elmptrab  24054  hausflimi  24207  hausflim  24208  alexsubALTlem3  24276  alexsubALTlem4  24277  ptcmplem2  24280  cnextcn  24294  cnextfres1  24295  tgphaus  24344  ustuqtop  24473  utopsnneip  24475  ucncn  24511  nrmmetd  24801  xrhmeo  25175  iscau2  25506  caucfil  25512  cmetcaulem  25517  bcth  25558  vitalilem3  25839  vitali  25842  i1f1lem  25918  itg11  25920  i1fres  25934  mbfi1fseq  25950  mbfi1flim  25952  itg2uba  25972  itg2splitlem  25977  isibl2  25995  cbvitg  26004  cbvitgv  26005  itgss3  26043  dvmptfsum  26203  rolle  26218  elply2  26422  plyexmo  26546  lgamgulmlem2  27267  prmorcht  27415  pclogsum  27452  dchr1  27494  lgsdir  27569  lgsdilem2  27570  lgsdi  27571  lgsne0  27572  lgsquadlem3  27619  lgsquad  27620  2sqlem8  27663  nosupcbv  27939  nosupno  27940  nosupdm  27941  nosupbnd1lem1  27945  noinfcbv  27954  noinfno  27955  noinfdm  27956  nocvxminlem  28020  legval  28927  legov  28928  tglineintmo  28990  tglowdim2ln  29000  ishpg  29117  lnopp2hpgb  29121  hpgerlem  29123  colopp  29127  elplngid  29140  lnincplng  29142  plngcp  29144  plngrot  29148  nhpmirhp  29156  lnperpexs  29190  ragraghl  29226  tgaaddcpbllem2  29230  tgaaddcpbllem3  29231  prlnghpg  29304  prlngmo  29312  tgaltai  29325  axcontlem1  29422  numedglnl  29602  uvtxnbgrvtx  29854  cusgrres  29909  wspniunwspnon  30392  rusgrnumwwlkb0  30443  frgr3vlem2  30755  3vfriswmgrlem  30758  fusgr2wsp2nb  30815  numclwlk2lem2f1o  30860  lpni  30962  pjhthmo  31784  chscllem2  32120  cbvdisjf  33045  2ndresdju  33123  fmptcof2  33131  aciunf1lem  33136  funcnv4mpt  33142  suppovss  33154  fpwrelmapffslem  33204  fsumiunle  33300  gsumwrd2dccatlem  33518  elrspunsn  33858  1arithufdlem3  33957  fedgmullem1  34140  fldextrspunlsp  34185  extdgfialglem2  34204  zarclssn  34384  esumcvg  34597  fiunelros  34686  measiun  34730  bnj1146  35301  bnj1185  35303  bnj1385  35342  bnj1014  35471  bnj1112  35493  bnj1123  35496  bnj1228  35521  bnj1326  35536  bnj1321  35537  bnj1384  35542  bnj1417  35551  bnj1497  35570  trssfir1om  35622  r1omhfb  35623  fineqvnttrclse  35651  axregscl  35655  setindregs  35657  trssfir1omregs  35663  r1omhfbregs  35664  onvf1odlem2  35702  onvf1odlem3  35703  gonarlem  35974  goalrlem  35976  goalr  35977  mrsubrn  36093  dfon2lem6  36366  dfbigcup2  36477  lineintmo  36738  cbvralvw2  36847  cbvrexvw2  36848  cbvrmovw2  36849  cbvreuvw2  36850  cbvmptvw2  36855  cbvprodvw2  36868  cbvrmodavw  36873  cbvreudavw  36874  cbvrabdavw  36882  cbvmptdavw  36888  cbvriotadavw  36891  cbvixpdavw  36899  cbvproddavw  36901  cbvitgdavw  36902  cbvrabdavw2  36906  cbvmptdavw2  36909  cbvriotadavw2  36911  weiunlem  37083  dfttc4  37150  mh-infprim2bi  37167  eleq2w2ALT  37792  bj-idres  37913  mptsnunlem  38093  wl-dfcleq  38269  wl-dfclel  38270  ptrest  38369  poimirlem25  38395  mblfinlem2  38408  mblfinlem3  38409  mblfinlem4  38410  ismblfin  38411  mbfposadd  38417  itg2addnclem  38421  ftc1anclem5  38447  ftc1anclem6  38448  ftc1anclem7  38449  ftc1anc  38451  areacirclem5  38462  fdc1  38497  inxprnres  39047  fsumshftd  39826  pmapglb  40644  polval2N  40780  osumcllem4N  40833  pexmidlem1N  40844  dih1dimatlem  42203  mapdh9a  42663  mapdh9aOLDN  42664  sticksstones2  43014  fsuppind  43437  fphpd  43658  fphpdo  43659  pellex  43677  setindtrs  43867  dford3lem2  43869  fnwe2lem2  43893  mendlmod  44031  cantnfub  44163  tfsconcat0i  44187  rababg  44415  fsovrfovd  44850  fsovcnvlem  44854  trfr  45786  elunif  45851  iunincfi  45927  cbvmpo2  45930  cbvmpo1  45931  disjf1  46016  wessf1ornlem  46018  disjinfi  46025  supxrleubrnmptf  46280  monoordxr  46311  monoord2xr  46313  fsummulc1f  46402  fsumnncl  46403  fsumf1of  46405  fsumiunss  46406  fsumreclf  46407  fsumlessf  46408  fsumsermpt  46410  fmulcl  46412  fmul01lt1lem2  46416  fprodexp  46425  fprodabs2  46426  climmulf  46435  climexp  46436  climrecf  46440  climinff  46442  climaddf  46446  mullimc  46447  limcperiod  46459  sumnnodd  46461  neglimc  46476  addlimc  46477  climsubmpt  46489  climreclf  46493  climeldmeqmpt  46497  climfveqmpt  46500  fnlimfvre  46503  climfveqf  46509  climfveqmpt3  46511  climeldmeqf  46512  climeqf  46517  climeldmeqmpt3  46518  climinf2  46536  limsupequz  46552  limsupequzmptf  46560  lmbr3  46576  cnrefiisp  46659  cncfshift  46703  fprodcncf  46729  dvmptmulf  46766  dvmptfprod  46774  dvnprodlem1  46775  dvnprodlem3  46777  stoweidlem16  46845  stoweidlem34  46863  stoweidlem62  46891  dirkercncflem2  46933  fourierdlem12  46948  fourierdlem15  46951  fourierdlem34  46970  fourierdlem50  46985  fourierdlem73  47008  fourierdlem94  47029  fourierdlem112  47047  fourierdlem113  47048  intsaluni  47158  sge0lempt  47239  sge0iunmptlemfi  47242  sge0iunmptlemre  47244  sge0iunmpt  47247  sge0ltfirpmpt2  47255  sge0isummpt2  47261  sge0xaddlem2  47263  sge0xadd  47264  meadjiun  47295  voliunsge0lem  47301  meaiuninclem  47309  meaiunincf  47312  meaiuninc3v  47313  meaiuninc3  47314  meaiininclem  47315  meaiininc  47316  isomennd  47360  ovn0lem  47394  sge0hsphoire  47418  hoidmvlelem1  47424  hoidmvlelem2  47425  hoidmvlelem3  47426  hoidmvlelem5  47428  hspmbllem2  47456  hoimbl2  47494  vonhoire  47501  vonioo  47511  vonicc  47514  vonn0ioo2  47519  vonn0icc2  47521  pimincfltioc  47545  salpreimagtlt  47559  smflimlem4  47603  ormkglobd  47706  sinnpoly  47760  rexrsb  47989  ichexmpl2  48371  ichnreuop  48373  sbgoldbm  48701  bgoldbnnsum3prm  48721  tgoldbach  48734  srhmsubcALTV  49241  cbvmpox2  49267  mo0sn  49745  f1omoOLD  49821  isthincd2lem1  50352  thincmo  50355  euendfunc  50453