Theorem eleq1w 2816

Description: Weaker version of eleq1 2821 (but more general than elequ1 2113) not depending on ax-ext 2703 nor df-cleq 2724.

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2810

This theorem is referenced by:  clelsb1  2860  cleqh  2863  nfcjust  2884  nfcr  2888  nfcriOLD  2893  nfcriOLDOLD  2894  cleqf  2934  rspw  3233  cbvralvw  3234  cbvrexvw  3235  cbvralfw  3301  cbvralfwOLD  3320  cbvralf  3356  ralcom2  3373  moel  3398  cbvrmovw  3399  cbvreuvw  3400  moelOLD  3401  cbvrmow  3405  cbvreuwOLD  3412  cbvreu  3424  cbvrabv  3442  rabrabi  3450  cbvrabw  3467  nfrab  3472  cbvrab  3473  reu2  3721  reu6  3722  rmo4  3726  reu8  3729  2reu5  3754  ru  3776  csbied  3931  difjust  3950  unjust  3952  injust  3954  dfss2f  3972  dfdif3  4114  eqeuel  4362  rabeq0w  4383  disj  4447  reldisj  4451  ralidmw  4507  dfif6  4531  rabsnifsb  4726  eluniab  4923  unissb  4943  elintabOLD  4963  uniintsn  4991  dfiun2g  5033  dfiunv2  5038  disjxun  5146  cbvmptf  5257  cbvmptfg  5258  cbvmptv  5261  dftr2c  5268  isso2i  5623  dfres2  6041  imai  6073  frpoinsg  6344  wfisgOLD  6355  tz7.7  6390  fvn0ssdmfun  7076  fmptco  7126  cbvriotaw  7373  cbvriotavw  7374  cbvriota  7378  cbvmpox  7501  tfis  7843  tfindes  7851  peano5  7883  findes  7892  dfoprab4f  8041  fmpox  8052  xpord2indlem  8132  poseq  8143  soseq  8144  wfrlem10OLD  8317  smogt  8366  resixpfo  8929  ixpsnf1o  8931  dom2lem  8987  mapsnend  9035  pw2f1olem  9075  pssnn  9167  ssfi  9172  findcard3  9284  findcard3OLD  9285  ordiso2  9509  elirrv  9590  cantnflem1d  9682  cantnf  9687  setind  9728  frinsg  9745  tz9.12lem3  9783  infxpen  10008  dfac12lem2  10138  kmlem14  10157  cfsmolem  10264  sornom  10271  isf32lem9  10355  axdc2  10443  fpwwe2lem7  10631  fpwwe2  10637  wunex2  10732  dedekindle  11377  wloglei  11745  uzind4s  12891  seqof2  14025  reuccatpfxs1  14696  shftfn  15019  rexuz3  15294  zsum  15663  fsum  15665  sumss  15669  sumss2  15671  fsumcvg2  15672  fsumser  15675  fsumclf  15683  fsumsplitf  15687  isumless  15790  prodfdiv  15841  cbvprod  15858  zprod  15880  fprod  15884  fprodntriv  15885  prodss  15890  fprod2dlem  15923  fproddivf  15930  fprodsplitf  15931  rpnnen2lem10  16165  cpnnen  16171  sumeven  16329  sumodd  16330  sadcp1  16395  smupp1  16420  pcmptdvds  16826  prmreclem2  16849  prmreclem5  16852  prmreclem6  16853  prmrec  16854  prmdvdsprmo  16974  iscatd2  17624  initoeu2  17965  yoniso  18237  sgrpidmnd  18629  mndind  18708  eqg0subg  19072  symggen  19337  dprd2d2  19913  isdrngrd  20390  isdrngrdOLD  20392  lbspss  20692  frlmphl  21335  frlmup1  21352  opsrtoslem1  21615  mdetralt  22109  mdetralt2  22110  mdetunilem2  22114  maducoeval2  22141  chfacfscmulgsum  22361  chfacfpmmulgsum  22365  isclo2  22591  neiptopnei  22635  ptcldmpt  23117  elmptrab  23330  hausflimi  23483  hausflim  23484  alexsubALTlem3  23552  alexsubALTlem4  23553  ptcmplem2  23556  cnextcn  23570  cnextfres1  23571  tgphaus  23620  ustuqtop  23750  utopsnneip  23752  ucncn  23789  nrmmetd  24082  xrhmeo  24461  iscau2  24793  caucfil  24799  cmetcaulem  24804  bcth  24845  vitalilem3  25126  vitali  25129  i1f1lem  25205  itg11  25207  i1fres  25222  mbfi1fseq  25238  mbfi1flim  25240  itg2uba  25260  itg2splitlem  25265  isibl2  25283  cbvitg  25292  itgss3  25331  dvmptfsum  25491  rolle  25506  elply2  25709  plyexmo  25825  lgamgulmlem2  26531  prmorcht  26679  pclogsum  26715  dchr1  26757  lgsdir  26832  lgsdilem2  26833  lgsdi  26834  lgsne0  26835  lgsquadlem3  26882  lgsquad  26883  2sqlem8  26926  nosupcbv  27202  nosupno  27203  nosupdm  27204  nosupbnd1lem1  27208  noinfcbv  27217  noinfno  27218  noinfdm  27219  nocvxminlem  27276  legval  27832  legov  27833  tglineintmo  27890  tglowdim2ln  27899  ishpg  28007  lnopp2hpgb  28011  hpgerlem  28013  colopp  28017  axcontlem1  28219  numedglnl  28401  uvtxnbgrvtx  28647  cusgrres  28702  wspniunwspnon  29174  rusgrnumwwlkb0  29222  frgr3vlem2  29524  3vfriswmgrlem  29527  fusgr2wsp2nb  29584  numclwlk2lem2f1o  29629  lpni  29728  pjhthmo  30550  chscllem2  30886  cbvdisjf  31797  2ndresdju  31869  fmptcof2  31877  aciunf1lem  31882  funcnv4mpt  31889  suppovss  31901  fpwrelmapffslem  31952  fsumiunle  32030  elrspunsn  32542  fedgmullem1  32709  zarclssn  32848  esumcvg  33079  fiunelros  33167  measiun  33211  bnj1146  33797  bnj1185  33799  bnj1385  33838  bnj1014  33967  bnj1112  33989  bnj1123  33992  bnj1228  34017  bnj1326  34032  bnj1321  34033  bnj1384  34038  bnj1417  34047  bnj1497  34066  gonarlem  34380  goalrlem  34382  goalr  34383  mrsubrn  34499  dfon2lem6  34755  dfbigcup2  34866  lineintmo  35124  eleq2w2ALT  35923  bj-idres  36036  mptsnunlem  36214  ptrest  36482  poimirlem25  36508  mblfinlem2  36521  mblfinlem3  36522  mblfinlem4  36523  ismblfin  36524  mbfposadd  36530  itg2addnclem  36534  ftc1anclem5  36560  ftc1anclem6  36561  ftc1anclem7  36562  ftc1anc  36564  areacirclem5  36575  fdc1  36609  inxprnres  37156  fsumshftd  37817  pmapglb  38636  polval2N  38772  osumcllem4N  38825  pexmidlem1N  38836  dih1dimatlem  40195  mapdh9a  40655  mapdh9aOLDN  40656  sticksstones2  40958  elrab2w  41022  selvvvval  41159  fsuppind  41164  fphpd  41544  fphpdo  41545  pellex  41563  setindtrs  41754  dford3lem2  41756  fnwe2lem2  41783  mendlmod  41925  cantnfub  42061  tfsconcat0i  42085  rababg  42315  fsovrfovd  42750  fsovcnvlem  42754  scottabf  42989  elunif  43690  iunincfi  43773  cbvmpo2  43776  cbvmpo1  43777  disjf1  43870  wessf1ornlem  43872  disjinfi  43881  supxrleubrnmptf  44151  monoordxr  44183  monoord2xr  44185  fsummulc1f  44277  fsumnncl  44278  fsumf1of  44280  fsumiunss  44281  fsumreclf  44282  fsumlessf  44283  fsumsermpt  44285  fmulcl  44287  fmul01lt1lem2  44291  fprodexp  44300  fprodabs2  44301  climmulf  44310  climexp  44311  climrecf  44315  climinff  44317  climaddf  44321  mullimc  44322  limcperiod  44334  sumnnodd  44336  neglimc  44353  addlimc  44354  climsubmpt  44366  climreclf  44370  climeldmeqmpt  44374  climfveqmpt  44377  fnlimfvre  44380  climfveqf  44386  climfveqmpt3  44388  climeldmeqf  44389  climeqf  44394  climeldmeqmpt3  44395  climinf2  44413  limsupequz  44429  limsupequzmptf  44437  lmbr3  44453  cnrefiisp  44536  cncfshift  44580  fprodcncf  44606  dvmptmulf  44643  dvmptfprod  44651  dvnprodlem1  44652  dvnprodlem3  44654  stoweidlem16  44722  stoweidlem34  44740  stoweidlem62  44768  dirkercncflem2  44810  fourierdlem12  44825  fourierdlem15  44828  fourierdlem34  44847  fourierdlem50  44862  fourierdlem73  44885  fourierdlem94  44906  fourierdlem112  44924  fourierdlem113  44925  intsaluni  45035  sge0lempt  45116  sge0iunmptlemfi  45119  sge0iunmptlemre  45121  sge0iunmpt  45124  sge0ltfirpmpt2  45132  sge0isummpt2  45138  sge0xaddlem2  45140  sge0xadd  45141  meadjiun  45172  voliunsge0lem  45178  meaiuninclem  45186  meaiunincf  45189  meaiuninc3v  45190  meaiuninc3  45191  meaiininclem  45192  meaiininc  45193  isomennd  45237  ovn0lem  45271  sge0hsphoire  45295  hoidmvlelem1  45301  hoidmvlelem2  45302  hoidmvlelem3  45303  hoidmvlelem5  45305  hspmbllem2  45333  hoimbl2  45371  vonhoire  45378  vonioo  45388  vonicc  45391  vonn0ioo2  45396  vonn0icc2  45398  pimincfltioc  45422  salpreimagtlt  45436  smflimlem4  45480  rexrsb  45798  ichexmpl2  46128  ichnreuop  46130  sbgoldbm  46442  bgoldbnnsum3prm  46462  tgoldbach  46475  srhmsubc  46964  srhmsubcALTV  46982  cbvmpox2  47001  mo0sn  47490  f1omo  47517  isthincd2lem1  47637  thincmo  47639