Theorem eleq1w 2811

Description: Weaker version of eleq1 2816 (but more general than elequ1 2116) not depending on ax-ext 2701 nor df-cleq 2721.

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

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

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 2008  ax-8 2111

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

This theorem is referenced by:  clelsb1  2855  cleqh  2857  nfcjust  2877  nfcr  2881  cleqf  2920  rspw  3212  cbvralvw  3213  cbvrexvw  3214  cbvralfw  3276  cbvralsvw  3287  cbvralf  3331  ralcom2  3348  moel  3373  cbvrmovw  3374  cbvreuvw  3375  cbvrmow  3378  cbvreu  3394  cbvrabv  3413  rabrabi  3422  cbvrabw  3438  cbvrabwOLD  3439  nfrab  3442  cbvrab  3443  elrab2w  3660  reu2  3693  reu6  3694  rmo4  3698  reu8  3701  2reu5  3726  ruOLD  3749  csbied  3895  difjust  3913  unjust  3915  injust  3917  dfss2  3929  dfssf  3934  dfdif3OLD  4077  eqeuel  4324  rabeq0w  4346  disj  4409  reldisj  4412  ralidmw  4467  dfif6  4487  rabsnifsb  4682  eluniab  4881  unissb  4899  elintabOLD  4919  uniintsn  4945  dfiun2g  4990  dfiunv2  4994  disjxun  5100  cbvmptf  5202  cbvmptfg  5203  cbvmptv  5206  dftr2c  5212  isso2i  5576  dfres2  6001  imai  6034  frpoinsg  6304  tz7.7  6346  fvn0ssdmfun  7028  fmptco  7083  cbvriotaw  7335  cbvriotavw  7336  cbvriota  7339  cbvmpox  7462  cbvmpov  7464  tfis  7811  tfindes  7819  peano5  7849  findes  7856  dfoprab4f  8014  fmpox  8025  xpord2indlem  8103  poseq  8114  soseq  8115  smogt  8313  resixpfo  8886  ixpsnf1o  8888  dom2lem  8940  mapsnend  8984  pw2f1olem  9022  pssnn  9109  ssfi  9114  findcard3  9205  findcard3OLD  9206  ordiso2  9444  elirrv  9525  cantnflem1d  9617  cantnf  9622  setind  9663  frinsg  9680  tz9.12lem3  9718  infxpen  9943  dfac5lem4  10055  dfac12lem2  10074  kmlem14  10093  cfsmolem  10199  sornom  10206  isf32lem9  10290  axdc2  10378  fpwwe2lem7  10566  fpwwe2  10572  wunex2  10667  dedekindle  11314  wloglei  11686  uzind4s  12843  seqof2  14001  reuccatpfxs1  14688  shftfn  15015  rexuz3  15291  zsum  15660  fsum  15662  sumss  15666  sumss2  15668  fsumcvg2  15669  fsumser  15672  fsumclf  15680  fsumsplitf  15684  isumless  15787  prodfdiv  15838  cbvprod  15855  cbvprodv  15856  zprod  15879  fprod  15883  fprodntriv  15884  prodss  15889  fprod2dlem  15922  fproddivf  15929  fprodsplitf  15930  rpnnen2lem10  16167  cpnnen  16173  sumeven  16333  sumodd  16334  sadcp1  16401  smupp1  16426  pcmptdvds  16841  prmreclem2  16864  prmreclem5  16867  prmreclem6  16868  prmrec  16869  prmdvdsprmo  16989  iscatd2  17618  initoeu2  17954  yoniso  18222  sgrpidmnd  18642  mndind  18731  eqg0subg  19104  symggen  19376  dprd2d2  19952  srhmsubc  20565  isdrngrd  20651  isdrngrdOLD  20653  lbspss  20965  frlmphl  21666  frlmup1  21683  opsrtoslem1  21938  mdetralt  22471  mdetralt2  22472  mdetunilem2  22476  maducoeval2  22503  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  isclo2  22951  neiptopnei  22995  ptcldmpt  23477  elmptrab  23690  hausflimi  23843  hausflim  23844  alexsubALTlem3  23912  alexsubALTlem4  23913  ptcmplem2  23916  cnextcn  23930  cnextfres1  23931  tgphaus  23980  ustuqtop  24110  utopsnneip  24112  ucncn  24148  nrmmetd  24438  xrhmeo  24820  iscau2  25153  caucfil  25159  cmetcaulem  25164  bcth  25205  vitalilem3  25487  vitali  25490  i1f1lem  25566  itg11  25568  i1fres  25582  mbfi1fseq  25598  mbfi1flim  25600  itg2uba  25620  itg2splitlem  25625  isibl2  25643  cbvitg  25653  cbvitgv  25654  itgss3  25692  dvmptfsum  25855  rolle  25870  elply2  26077  plyexmo  26197  lgamgulmlem2  26916  prmorcht  27064  pclogsum  27102  dchr1  27144  lgsdir  27219  lgsdilem2  27220  lgsdi  27221  lgsne0  27222  lgsquadlem3  27269  lgsquad  27270  2sqlem8  27313  nosupcbv  27590  nosupno  27591  nosupdm  27592  nosupbnd1lem1  27596  noinfcbv  27605  noinfno  27606  noinfdm  27607  nocvxminlem  27665  legval  28487  legov  28488  tglineintmo  28545  tglowdim2ln  28554  ishpg  28662  lnopp2hpgb  28666  hpgerlem  28668  colopp  28672  axcontlem1  28867  numedglnl  29047  uvtxnbgrvtx  29296  cusgrres  29352  wspniunwspnon  29826  rusgrnumwwlkb0  29874  frgr3vlem2  30176  3vfriswmgrlem  30179  fusgr2wsp2nb  30236  numclwlk2lem2f1o  30281  lpni  30382  pjhthmo  31204  chscllem2  31540  cbvdisjf  32473  2ndresdju  32546  fmptcof2  32554  aciunf1lem  32559  funcnv4mpt  32566  suppovss  32577  fpwrelmapffslem  32628  fsumiunle  32727  gsumwrd2dccatlem  32979  elrspunsn  33373  1arithufdlem3  33490  fedgmullem1  33598  fldextrspunlsp  33642  zarclssn  33836  esumcvg  34049  fiunelros  34137  measiun  34181  bnj1146  34754  bnj1185  34756  bnj1385  34795  bnj1014  34924  bnj1112  34946  bnj1123  34949  bnj1228  34974  bnj1326  34989  bnj1321  34990  bnj1384  34995  bnj1417  35004  bnj1497  35023  onvf1odlem2  35064  onvf1odlem3  35065  gonarlem  35354  goalrlem  35356  goalr  35357  mrsubrn  35473  dfon2lem6  35749  dfbigcup2  35860  lineintmo  36118  cbvralvw2  36187  cbvrexvw2  36188  cbvrmovw2  36189  cbvreuvw2  36190  cbvmptvw2  36195  cbvprodvw2  36208  cbvrmodavw  36213  cbvreudavw  36214  cbvrabdavw  36222  cbvmptdavw  36228  cbvriotadavw  36231  cbvixpdavw  36239  cbvproddavw  36241  cbvitgdavw  36242  cbvrabdavw2  36246  cbvmptdavw2  36249  cbvriotadavw2  36251  weiunlem2  36424  eleq2w2ALT  37008  bj-idres  37121  mptsnunlem  37299  ptrest  37586  poimirlem25  37612  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  mbfposadd  37634  itg2addnclem  37638  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anc  37668  areacirclem5  37679  fdc1  37713  inxprnres  38253  fsumshftd  38918  pmapglb  39737  polval2N  39873  osumcllem4N  39926  pexmidlem1N  39937  dih1dimatlem  41296  mapdh9a  41756  mapdh9aOLDN  41757  sticksstones2  42108  selvvvval  42546  fsuppind  42551  fphpd  42777  fphpdo  42778  pellex  42796  setindtrs  42987  dford3lem2  42989  fnwe2lem2  43013  mendlmod  43151  cantnfub  43283  tfsconcat0i  43307  rababg  43536  fsovrfovd  43971  fsovcnvlem  43975  scottabf  44202  trfr  44925  elunif  44983  iunincfi  45061  cbvmpo2  45064  cbvmpo1  45065  disjf1  45150  wessf1ornlem  45152  disjinfi  45159  supxrleubrnmptf  45420  monoordxr  45451  monoord2xr  45453  fsummulc1f  45542  fsumnncl  45543  fsumf1of  45545  fsumiunss  45546  fsumreclf  45547  fsumlessf  45548  fsumsermpt  45550  fmulcl  45552  fmul01lt1lem2  45556  fprodexp  45565  fprodabs2  45566  climmulf  45575  climexp  45576  climrecf  45580  climinff  45582  climaddf  45586  mullimc  45587  limcperiod  45599  sumnnodd  45601  neglimc  45618  addlimc  45619  climsubmpt  45631  climreclf  45635  climeldmeqmpt  45639  climfveqmpt  45642  fnlimfvre  45645  climfveqf  45651  climfveqmpt3  45653  climeldmeqf  45654  climeqf  45659  climeldmeqmpt3  45660  climinf2  45678  limsupequz  45694  limsupequzmptf  45702  lmbr3  45718  cnrefiisp  45801  cncfshift  45845  fprodcncf  45871  dvmptmulf  45908  dvmptfprod  45916  dvnprodlem1  45917  dvnprodlem3  45919  stoweidlem16  45987  stoweidlem34  46005  stoweidlem62  46033  dirkercncflem2  46075  fourierdlem12  46090  fourierdlem15  46093  fourierdlem34  46112  fourierdlem50  46127  fourierdlem73  46150  fourierdlem94  46171  fourierdlem112  46189  fourierdlem113  46190  intsaluni  46300  sge0lempt  46381  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0iunmpt  46389  sge0ltfirpmpt2  46397  sge0isummpt2  46403  sge0xaddlem2  46405  sge0xadd  46406  meadjiun  46437  voliunsge0lem  46443  meaiuninclem  46451  meaiunincf  46454  meaiuninc3v  46455  meaiuninc3  46456  meaiininclem  46457  meaiininc  46458  isomennd  46502  ovn0lem  46536  sge0hsphoire  46560  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem5  46570  hspmbllem2  46598  hoimbl2  46636  vonhoire  46643  vonioo  46653  vonicc  46656  vonn0ioo2  46661  vonn0icc2  46663  pimincfltioc  46687  salpreimagtlt  46701  smflimlem4  46745  ormkglobd  46846  sinnpoly  46865  rexrsb  47074  ichexmpl2  47444  ichnreuop  47446  sbgoldbm  47758  bgoldbnnsum3prm  47778  tgoldbach  47791  srhmsubcALTV  48286  cbvmpox2  48297  mo0sn  48777  f1omoOLD  48855  isthincd2lem1  49387  thincmo  49390  euendfunc  49488