Theorem eleq1w 2820

Description: Weaker version of eleq1 2825 (but more general than elequ1 2117) not depending on ax-ext 2708 nor df-cleq 2729.

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∃wex 1787   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-clel 2816

This theorem is referenced by:  cleqh  2861  clelsb3  2865  nfcjust  2885  nfcr  2889  nfcriOLD  2894  nfcriOLDOLD  2895  cleqf  2935  rspw  3126  ralcom2  3275  nfrab  3298  moel  3335  cbvralfw  3344  cbvralfwOLD  3345  cbvralf  3347  cbvreuw  3351  cbvrmow  3352  cbvreu  3356  cbvralvw  3358  cbvrexvw  3359  cbvrmovw  3360  cbvreuvw  3361  cbvrabw  3400  cbvrab  3401  cbvrabv  3402  rabrabi  3403  ralab2OLD  3611  rexab2OLD  3614  reu2  3638  reu6  3639  rmo4  3643  reu8  3646  2reu5  3671  ru  3693  csbied  3849  difjust  3868  unjust  3870  injust  3872  dfss2f  3890  dfdif3  4029  eqeuel  4277  rabeq0w  4298  disj  4362  reldisj  4366  ralidmw  4419  dfif6  4442  rabsnifsb  4638  eluniab  4834  elintab  4870  uniintsn  4898  dfiunv2  4944  disjxun  5051  cbvmptf  5154  cbvmptfg  5155  isso2i  5503  dfres2  5909  imai  5942  frpoinsg  6197  wfisg  6205  tz7.7  6239  fvn0ssdmfun  6895  fmptco  6944  cbvriotaw  7179  cbvriotavw  7180  cbvriota  7184  cbvmpox  7304  tfis  7633  tfindes  7641  peano5  7671  findes  7680  dfoprab4f  7826  fmpox  7837  wfrlem10  8064  smogt  8104  resixpfo  8617  ixpsnf1o  8619  dom2lem  8668  mapsnend  8713  pw2f1olem  8749  pssnn  8846  ssfi  8851  findcard3  8914  ordiso2  9131  elirrv  9212  cantnflem1d  9303  cantnf  9308  setind  9350  frinsg  9367  tz9.12lem3  9405  infxpen  9628  dfac12lem2  9758  kmlem14  9777  cfsmolem  9884  sornom  9891  isf32lem9  9975  axdc2  10063  fpwwe2lem7  10251  fpwwe2  10257  wunex2  10352  dedekindle  10996  wloglei  11364  uzind4s  12504  seqof2  13634  reuccatpfxs1  14312  shftfn  14636  rexuz3  14912  zsum  15282  fsum  15284  sumss  15288  sumss2  15290  fsumcvg2  15291  fsumser  15294  fsumclf  15302  fsumsplitf  15306  isumless  15409  prodfdiv  15460  cbvprod  15477  zprod  15499  fprod  15503  fprodntriv  15504  prodss  15509  fprod2dlem  15542  fproddivf  15549  fprodsplitf  15550  rpnnen2lem10  15784  cpnnen  15790  sumeven  15948  sumodd  15949  sadcp1  16014  smupp1  16039  pcmptdvds  16447  prmreclem2  16470  prmreclem5  16473  prmreclem6  16474  prmrec  16475  prmdvdsprmo  16595  iscatd2  17184  initoeu2  17522  yoniso  17793  sgrpidmnd  18178  mndind  18254  symggen  18862  dprd2d2  19431  isdrngrd  19793  lbspss  20119  frlmphl  20743  frlmup1  20760  opsrtoslem1  21012  mdetralt  21505  mdetralt2  21506  mdetunilem2  21510  maducoeval2  21537  chfacfscmulgsum  21757  chfacfpmmulgsum  21761  isclo2  21985  neiptopnei  22029  ptcldmpt  22511  elmptrab  22724  hausflimi  22877  hausflim  22878  alexsubALTlem3  22946  alexsubALTlem4  22947  ptcmplem2  22950  cnextcn  22964  cnextfres1  22965  tgphaus  23014  ustuqtop  23144  utopsnneip  23146  ucncn  23182  nrmmetd  23472  xrhmeo  23843  iscau2  24174  caucfil  24180  cmetcaulem  24185  bcth  24226  vitalilem3  24507  vitali  24510  i1f1lem  24586  itg11  24588  i1fres  24603  mbfi1fseq  24619  mbfi1flim  24621  itg2uba  24641  itg2splitlem  24646  isibl2  24664  cbvitg  24673  itgss3  24712  dvmptfsum  24872  rolle  24887  elply2  25090  plyexmo  25206  lgamgulmlem2  25912  prmorcht  26060  pclogsum  26096  dchr1  26138  lgsdir  26213  lgsdilem2  26214  lgsdi  26215  lgsne0  26216  lgsquadlem3  26263  lgsquad  26264  2sqlem8  26307  legval  26675  legov  26676  tglineintmo  26733  tglowdim2ln  26742  ishpg  26850  lnopp2hpgb  26854  hpgerlem  26856  colopp  26860  axcontlem1  27055  numedglnl  27235  uvtxnbgrvtx  27481  cusgrres  27536  wspniunwspnon  28007  rusgrnumwwlkb0  28055  frgr3vlem2  28357  3vfriswmgrlem  28360  fusgr2wsp2nb  28417  numclwlk2lem2f1o  28462  lpni  28561  pjhthmo  29383  chscllem2  29719  cbvdisjf  30629  2ndresdju  30705  fmptcof2  30714  aciunf1lem  30719  funcnv4mpt  30726  suppovss  30737  fpwrelmapffslem  30787  fsumiunle  30863  fedgmullem1  31424  zarclssn  31537  esumcvg  31766  fiunelros  31854  measiun  31898  bnj1146  32484  bnj1185  32486  bnj1385  32525  bnj1014  32654  bnj1112  32676  bnj1123  32679  bnj1228  32704  bnj1326  32719  bnj1321  32720  bnj1384  32725  bnj1417  32734  bnj1497  32753  gonarlem  33069  goalrlem  33071  goalr  33072  mrsubrn  33188  dfon2lem6  33483  xpord2ind  33531  xpord3ind  33537  poseq  33539  soseq  33540  nosupcbv  33642  nosupno  33643  nosupdm  33644  nosupbnd1lem1  33648  noinfcbv  33657  noinfno  33658  noinfdm  33659  nocvxminlem  33709  dfbigcup2  33938  lineintmo  34196  eleq2w2ALT  34957  bj-idres  35066  mptsnunlem  35246  ptrest  35513  poimirlem25  35539  mblfinlem2  35552  mblfinlem3  35553  mblfinlem4  35554  ismblfin  35555  mbfposadd  35561  itg2addnclem  35565  ftc1anclem5  35591  ftc1anclem6  35592  ftc1anclem7  35593  ftc1anc  35595  areacirclem5  35606  fdc1  35641  inxprnres  36164  fsumshftd  36703  pmapglb  37521  polval2N  37657  osumcllem4N  37710  pexmidlem1N  37721  dih1dimatlem  39080  mapdh9a  39540  mapdh9aOLDN  39541  sticksstones2  39825  elrab2w  39889  fsuppind  39989  fphpd  40341  fphpdo  40342  pellex  40360  setindtrs  40550  dford3lem2  40552  fnwe2lem2  40579  mendlmod  40721  rababg  40857  fsovrfovd  41294  fsovcnvlem  41298  scottabf  41531  elunif  42232  iunincfi  42317  cbvmpo2  42320  cbvmpo1  42321  disjf1  42393  wessf1ornlem  42395  disjinfi  42404  supxrleubrnmptf  42666  monoordxr  42698  monoord2xr  42700  fsummulc1f  42787  fsumnncl  42788  fsumf1of  42790  fsumiunss  42791  fsumreclf  42792  fsumlessf  42793  fsumsermpt  42795  fmulcl  42797  fmul01lt1lem2  42801  fprodexp  42810  fprodabs2  42811  climmulf  42820  climexp  42821  climrecf  42825  climinff  42827  climaddf  42831  mullimc  42832  limcperiod  42844  sumnnodd  42846  neglimc  42863  addlimc  42864  climsubmpt  42876  climreclf  42880  climeldmeqmpt  42884  climfveqmpt  42887  fnlimfvre  42890  climfveqf  42896  climfveqmpt3  42898  climeldmeqf  42899  climeqf  42904  climeldmeqmpt3  42905  climinf2  42923  limsupequz  42939  limsupequzmptf  42947  lmbr3  42963  cnrefiisp  43046  cncfshift  43090  fprodcncf  43116  dvmptmulf  43153  dvmptfprod  43161  dvnprodlem1  43162  dvnprodlem3  43164  stoweidlem16  43232  stoweidlem34  43250  stoweidlem62  43278  dirkercncflem2  43320  fourierdlem12  43335  fourierdlem15  43338  fourierdlem34  43357  fourierdlem50  43372  fourierdlem73  43395  fourierdlem94  43416  fourierdlem112  43434  fourierdlem113  43435  intsaluni  43543  sge0lempt  43623  sge0iunmptlemfi  43626  sge0iunmptlemre  43628  sge0iunmpt  43631  sge0ltfirpmpt2  43639  sge0isummpt2  43645  sge0xaddlem2  43647  sge0xadd  43648  meadjiun  43679  voliunsge0lem  43685  meaiuninclem  43693  meaiunincf  43696  meaiuninc3v  43697  meaiuninc3  43698  meaiininclem  43699  meaiininc  43700  isomennd  43744  ovn0lem  43778  sge0hsphoire  43802  hoidmvlelem1  43808  hoidmvlelem2  43809  hoidmvlelem3  43810  hoidmvlelem5  43812  hspmbllem2  43840  hoimbl2  43878  vonhoire  43885  vonioo  43895  vonicc  43898  vonn0ioo2  43903  vonn0icc2  43905  pimincfltioc  43925  salpreimagtlt  43938  smflimlem4  43981  rexrsb  44264  ichexmpl2  44595  ichnreuop  44597  sbgoldbm  44909  bgoldbnnsum3prm  44929  tgoldbach  44942  srhmsubc  45307  srhmsubcALTV  45325  cbvmpox2  45344  mo0sn  45834  f1omo  45861  isthincd2lem1  45981  thincmo  45983