Theorem eleq1w 2817

Description: Weaker version of eleq1 2822 (but more general than elequ1 2115) not depending on ax-ext 2707 nor df-cleq 2727.

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809

This theorem is referenced by:  clelsb1  2861  cleqh  2864  nfcjust  2884  nfcr  2888  cleqf  2927  rspw  3219  cbvralvw  3220  cbvrexvw  3221  cbvralfw  3284  cbvralsvw  3296  cbvralf  3339  ralcom2  3356  moel  3381  cbvrmovw  3382  cbvreuvw  3383  moelOLD  3384  cbvrmow  3388  cbvreuwOLD  3394  cbvreu  3407  cbvrabv  3426  rabrabi  3435  cbvrabw  3452  cbvrabwOLD  3453  nfrab  3457  cbvrab  3458  elrab2w  3675  reu2  3708  reu6  3709  rmo4  3713  reu8  3716  2reu5  3741  ruOLD  3764  csbied  3910  difjust  3928  unjust  3930  injust  3932  dfss2  3944  dfssf  3949  dfdif3OLD  4093  eqeuel  4340  rabeq0w  4362  disj  4425  reldisj  4428  ralidmw  4483  dfif6  4503  rabsnifsb  4698  eluniab  4897  unissb  4915  elintabOLD  4935  uniintsn  4961  dfiun2g  5006  dfiunv2  5011  disjxun  5117  cbvmptf  5221  cbvmptfg  5222  cbvmptv  5225  dftr2c  5232  isso2i  5598  dfres2  6028  imai  6061  frpoinsg  6332  wfisgOLD  6343  tz7.7  6378  fvn0ssdmfun  7063  fmptco  7118  cbvriotaw  7369  cbvriotavw  7370  cbvriota  7373  cbvmpox  7498  cbvmpov  7500  tfis  7848  tfindes  7856  peano5  7887  findes  7894  dfoprab4f  8053  fmpox  8064  xpord2indlem  8144  poseq  8155  soseq  8156  wfrlem10OLD  8330  smogt  8379  resixpfo  8948  ixpsnf1o  8950  dom2lem  9004  mapsnend  9048  pw2f1olem  9088  pssnn  9180  ssfi  9185  findcard3  9288  findcard3OLD  9289  ordiso2  9527  elirrv  9608  cantnflem1d  9700  cantnf  9705  setind  9746  frinsg  9763  tz9.12lem3  9801  infxpen  10026  dfac5lem4  10138  dfac12lem2  10157  kmlem14  10176  cfsmolem  10282  sornom  10289  isf32lem9  10373  axdc2  10461  fpwwe2lem7  10649  fpwwe2  10655  wunex2  10750  dedekindle  11397  wloglei  11767  uzind4s  12922  seqof2  14076  reuccatpfxs1  14763  shftfn  15090  rexuz3  15365  zsum  15732  fsum  15734  sumss  15738  sumss2  15740  fsumcvg2  15741  fsumser  15744  fsumclf  15752  fsumsplitf  15756  isumless  15859  prodfdiv  15910  cbvprod  15927  cbvprodv  15928  zprod  15951  fprod  15955  fprodntriv  15956  prodss  15961  fprod2dlem  15994  fproddivf  16001  fprodsplitf  16002  rpnnen2lem10  16239  cpnnen  16245  sumeven  16404  sumodd  16405  sadcp1  16472  smupp1  16497  pcmptdvds  16912  prmreclem2  16935  prmreclem5  16938  prmreclem6  16939  prmrec  16940  prmdvdsprmo  17060  iscatd2  17691  initoeu2  18027  yoniso  18295  sgrpidmnd  18715  mndind  18804  eqg0subg  19177  symggen  19449  dprd2d2  20025  srhmsubc  20638  isdrngrd  20724  isdrngrdOLD  20726  lbspss  21038  frlmphl  21739  frlmup1  21756  opsrtoslem1  22011  mdetralt  22544  mdetralt2  22545  mdetunilem2  22549  maducoeval2  22576  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  isclo2  23024  neiptopnei  23068  ptcldmpt  23550  elmptrab  23763  hausflimi  23916  hausflim  23917  alexsubALTlem3  23985  alexsubALTlem4  23986  ptcmplem2  23989  cnextcn  24003  cnextfres1  24004  tgphaus  24053  ustuqtop  24183  utopsnneip  24185  ucncn  24221  nrmmetd  24511  xrhmeo  24893  iscau2  25227  caucfil  25233  cmetcaulem  25238  bcth  25279  vitalilem3  25561  vitali  25564  i1f1lem  25640  itg11  25642  i1fres  25656  mbfi1fseq  25672  mbfi1flim  25674  itg2uba  25694  itg2splitlem  25699  isibl2  25717  cbvitg  25727  cbvitgv  25728  itgss3  25766  dvmptfsum  25929  rolle  25944  elply2  26151  plyexmo  26271  lgamgulmlem2  26990  prmorcht  27138  pclogsum  27176  dchr1  27218  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  lgsquadlem3  27343  lgsquad  27344  2sqlem8  27387  nosupcbv  27664  nosupno  27665  nosupdm  27666  nosupbnd1lem1  27670  noinfcbv  27679  noinfno  27680  noinfdm  27681  nocvxminlem  27739  legval  28509  legov  28510  tglineintmo  28567  tglowdim2ln  28576  ishpg  28684  lnopp2hpgb  28688  hpgerlem  28690  colopp  28694  axcontlem1  28889  numedglnl  29069  uvtxnbgrvtx  29318  cusgrres  29374  wspniunwspnon  29851  rusgrnumwwlkb0  29899  frgr3vlem2  30201  3vfriswmgrlem  30204  fusgr2wsp2nb  30261  numclwlk2lem2f1o  30306  lpni  30407  pjhthmo  31229  chscllem2  31565  cbvdisjf  32498  2ndresdju  32573  fmptcof2  32581  aciunf1lem  32586  funcnv4mpt  32593  suppovss  32604  fpwrelmapffslem  32655  fsumiunle  32754  gsumwrd2dccatlem  33006  elrspunsn  33390  1arithufdlem3  33507  fedgmullem1  33615  fldextrspunlsp  33661  zarclssn  33850  esumcvg  34063  fiunelros  34151  measiun  34195  bnj1146  34768  bnj1185  34770  bnj1385  34809  bnj1014  34938  bnj1112  34960  bnj1123  34963  bnj1228  34988  bnj1326  35003  bnj1321  35004  bnj1384  35009  bnj1417  35018  bnj1497  35037  gonarlem  35362  goalrlem  35364  goalr  35365  mrsubrn  35481  dfon2lem6  35752  dfbigcup2  35863  lineintmo  36121  cbvralvw2  36190  cbvrexvw2  36191  cbvrmovw2  36192  cbvreuvw2  36193  cbvmptvw2  36198  cbvprodvw2  36211  cbvrmodavw  36216  cbvreudavw  36217  cbvrabdavw  36225  cbvmptdavw  36231  cbvriotadavw  36234  cbvixpdavw  36242  cbvproddavw  36244  cbvitgdavw  36245  cbvrabdavw2  36249  cbvmptdavw2  36252  cbvriotadavw2  36254  weiunlem2  36427  eleq2w2ALT  37011  bj-idres  37124  mptsnunlem  37302  ptrest  37589  poimirlem25  37615  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  mbfposadd  37637  itg2addnclem  37641  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anc  37671  areacirclem5  37682  fdc1  37716  inxprnres  38256  fsumshftd  38916  pmapglb  39735  polval2N  39871  osumcllem4N  39924  pexmidlem1N  39935  dih1dimatlem  41294  mapdh9a  41754  mapdh9aOLDN  41755  sticksstones2  42106  selvvvval  42555  fsuppind  42560  fphpd  42786  fphpdo  42787  pellex  42805  setindtrs  42996  dford3lem2  42998  fnwe2lem2  43022  mendlmod  43160  cantnfub  43292  tfsconcat0i  43316  rababg  43545  fsovrfovd  43980  fsovcnvlem  43984  scottabf  44212  trfr  44935  elunif  44988  iunincfi  45066  cbvmpo2  45069  cbvmpo1  45070  disjf1  45155  wessf1ornlem  45157  disjinfi  45164  supxrleubrnmptf  45426  monoordxr  45457  monoord2xr  45459  fsummulc1f  45548  fsumnncl  45549  fsumf1of  45551  fsumiunss  45552  fsumreclf  45553  fsumlessf  45554  fsumsermpt  45556  fmulcl  45558  fmul01lt1lem2  45562  fprodexp  45571  fprodabs2  45572  climmulf  45581  climexp  45582  climrecf  45586  climinff  45588  climaddf  45592  mullimc  45593  limcperiod  45605  sumnnodd  45607  neglimc  45624  addlimc  45625  climsubmpt  45637  climreclf  45641  climeldmeqmpt  45645  climfveqmpt  45648  fnlimfvre  45651  climfveqf  45657  climfveqmpt3  45659  climeldmeqf  45660  climeqf  45665  climeldmeqmpt3  45666  climinf2  45684  limsupequz  45700  limsupequzmptf  45708  lmbr3  45724  cnrefiisp  45807  cncfshift  45851  fprodcncf  45877  dvmptmulf  45914  dvmptfprod  45922  dvnprodlem1  45923  dvnprodlem3  45925  stoweidlem16  45993  stoweidlem34  46011  stoweidlem62  46039  dirkercncflem2  46081  fourierdlem12  46096  fourierdlem15  46099  fourierdlem34  46118  fourierdlem50  46133  fourierdlem73  46156  fourierdlem94  46177  fourierdlem112  46195  fourierdlem113  46196  intsaluni  46306  sge0lempt  46387  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0iunmpt  46395  sge0ltfirpmpt2  46403  sge0isummpt2  46409  sge0xaddlem2  46411  sge0xadd  46412  meadjiun  46443  voliunsge0lem  46449  meaiuninclem  46457  meaiunincf  46460  meaiuninc3v  46461  meaiuninc3  46462  meaiininclem  46463  meaiininc  46464  isomennd  46508  ovn0lem  46542  sge0hsphoire  46566  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem5  46576  hspmbllem2  46604  hoimbl2  46642  vonhoire  46649  vonioo  46659  vonicc  46662  vonn0ioo2  46667  vonn0icc2  46669  pimincfltioc  46693  salpreimagtlt  46707  smflimlem4  46751  ormkglobd  46852  rexrsb  47077  ichexmpl2  47432  ichnreuop  47434  sbgoldbm  47746  bgoldbnnsum3prm  47766  tgoldbach  47779  srhmsubcALTV  48248  cbvmpox2  48259  mo0sn  48742  f1omo  48816  isthincd2lem1  49259  thincmo  49262  euendfunc  49359