Theorem eleq1w 2845

Description: Weaker version of eleq1 2850 (but more general than elequ1 2149) not depending on ax-ext 2734 nor df-cleq 2754.

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∃wex 1799   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-clel 2837

This theorem is referenced by:  clelsb1  2889  cleqh  2891  nfcjust  2910  nfcr  2914  cleqf  2952  rspw  3239  cbvralvw  3240  cbvrexvw  3241  cbvralfw  3302  cbvralsvw  3313  cbvralf  3347  ralcom2  3364  moel  3387  cbvrmovw  3388  cbvreuvw  3389  cbvrmow  3392  cbvreu  3406  cbvrabv  3424  rabrabi  3433  cbvrabw  3449  cbvrabwOLD  3450  nfrab  3452  cbvrab  3453  elrab2w  3655  reu2  3688  reu6  3689  rmo4  3693  reu8  3696  2reu5  3721  csbied  3888  difjust  3906  unjust  3908  injust  3910  dfss2  3922  dfssf  3927  dfdif3OLD  4072  eqeuel  4318  rabeq0w  4341  disj  4404  reldisj  4407  ralidmw  4470  dfif6  4483  rabsnifsb  4681  eluniab  4879  unissb  4899  uniintsn  4943  dfiun2g  4987  dfiunv2  4991  disjxun  5098  cbvmptf  5200  cbvmptfg  5201  cbvmptv  5204  dftr2c  5210  isso2i  5592  dfres2  6030  imai  6063  frpoinsg  6330  tz7.7  6372  fvn0ssdmfun  7055  fmptco  7111  cbvriotaw  7362  cbvriotavw  7363  cbvriota  7366  cbvmpox  7489  cbvmpov  7491  tfis  7835  tfindes  7843  peano5  7874  findes  7881  dfoprab4f  8037  fmpox  8048  xpord2indlem  8127  poseq  8138  soseq  8139  smogt  8338  resixpfo  8918  ixpsnf1o  8920  dom2lem  8973  mapsnend  9017  pw2f1olem  9053  pssnn  9137  ssfi  9141  findcard3  9227  ordiso2  9463  elirrvOLDOLD  9547  cantnflem1d  9643  cantnf  9648  setind  9702  frinsg  9709  tz9.12lem3  9747  infxpen  9970  dfac5lem4  10082  dfac12lem2  10101  kmlem14  10120  cfsmolem  10227  sornom  10234  isf32lem9  10318  axdc2  10406  fpwwe2lem7  10595  fpwwe2  10601  wunex2  10696  dedekindle  11347  wloglei  11719  uzind4s  12909  seqof2  14073  reuccatpfxs1  14760  shftfn  15086  rexuz3  15376  zsum  15745  fsum  15747  sumss  15751  sumss2  15753  fsumcvg2  15754  fsumser  15757  fsumclf  15765  fsumsplitf  15769  isumless  15875  prodfdiv  15926  cbvprod  15943  cbvprodv  15944  zprod  15967  fprod  15971  fprodntriv  15972  prodss  15977  fprod2dlem  16010  fproddivf  16017  fprodsplitf  16018  rpnnen2lem10  16255  cpnnen  16261  sumeven  16421  sumodd  16422  sadcp1  16489  smupp1  16514  pcmptdvds  16930  prmreclem2  16953  prmreclem5  16956  prmreclem6  16957  prmrec  16958  prmdvdsprmo  17078  iscatd2  17713  initoeu2  18049  yoniso  18317  sgrpidmnd  18773  mndind  18862  eqg0subg  19237  symggen  19510  dprd2d2  20086  srhmsubc  20726  isdrngrd  20812  isdrngrdOLD  20814  lbspss  21146  frlmphl  21830  frlmup1  21847  opsrtoslem1  22105  selvvvval  22192  mdetralt  22665  mdetralt2  22666  mdetunilem2  22670  maducoeval2  22697  chfacfscmulgsum  22917  chfacfpmmulgsum  22921  isclo2  23145  neiptopnei  23189  ptcldmpt  23671  elmptrab  23884  hausflimi  24037  hausflim  24038  alexsubALTlem3  24106  alexsubALTlem4  24107  ptcmplem2  24110  cnextcn  24124  cnextfres1  24125  tgphaus  24174  ustuqtop  24303  utopsnneip  24305  ucncn  24341  nrmmetd  24631  xrhmeo  25005  iscau2  25336  caucfil  25342  cmetcaulem  25347  bcth  25388  vitalilem3  25669  vitali  25672  i1f1lem  25748  itg11  25750  i1fres  25764  mbfi1fseq  25780  mbfi1flim  25782  itg2uba  25802  itg2splitlem  25807  isibl2  25825  cbvitg  25835  cbvitgv  25836  itgss3  25874  dvmptfsum  26034  rolle  26049  elply2  26253  plyexmo  26374  lgamgulmlem2  27091  prmorcht  27239  pclogsum  27276  dchr1  27318  lgsdir  27393  lgsdilem2  27394  lgsdi  27395  lgsne0  27396  lgsquadlem3  27443  lgsquad  27444  2sqlem8  27487  nosupcbv  27763  nosupno  27764  nosupdm  27765  nosupbnd1lem1  27769  noinfcbv  27778  noinfno  27779  noinfdm  27780  nocvxminlem  27844  legval  28750  legov  28751  tglineintmo  28808  tglowdim2ln  28818  ishpg  28929  lnopp2hpgb  28933  hpgerlem  28935  colopp  28939  elplngid  28986  lnincplng  28988  plngcp  28990  plngrot  28994  axcontlem1  29162  numedglnl  29342  uvtxnbgrvtx  29591  cusgrres  29646  wspniunwspnon  30120  rusgrnumwwlkb0  30171  frgr3vlem2  30473  3vfriswmgrlem  30476  fusgr2wsp2nb  30533  numclwlk2lem2f1o  30578  lpni  30680  pjhthmo  31502  chscllem2  31838  cbvdisjf  32768  2ndresdju  32848  fmptcof2  32856  aciunf1lem  32861  funcnv4mpt  32867  suppovss  32880  fpwrelmapffslem  32931  fsumiunle  33028  gsumwrd2dccatlem  33254  elrspunsn  33612  1arithufdlem3  33739  fedgmullem1  33923  fldextrspunlsp  33968  extdgfialglem2  33987  zarclssn  34167  esumcvg  34380  fiunelros  34468  measiun  34512  bnj1146  35083  bnj1185  35085  bnj1385  35124  bnj1014  35253  bnj1112  35275  bnj1123  35278  bnj1228  35303  bnj1326  35318  bnj1321  35319  bnj1384  35324  bnj1417  35333  bnj1497  35352  trssfir1om  35404  r1omhfb  35405  fineqvnttrclse  35417  axregscl  35421  setindregs  35423  trssfir1omregs  35429  r1omhfbregs  35430  onvf1odlem2  35444  onvf1odlem3  35445  gonarlem  35741  goalrlem  35743  goalr  35744  mrsubrn  35860  dfon2lem6  36133  dfbigcup2  36244  lineintmo  36504  cbvralvw2  36583  cbvrexvw2  36584  cbvrmovw2  36585  cbvreuvw2  36586  cbvmptvw2  36591  cbvprodvw2  36604  cbvrmodavw  36609  cbvreudavw  36610  cbvrabdavw  36618  cbvmptdavw  36624  cbvriotadavw  36627  cbvixpdavw  36635  cbvproddavw  36637  cbvitgdavw  36638  cbvrabdavw2  36642  cbvmptdavw2  36645  cbvriotadavw2  36647  weiunlem  36820  dfttc4  36887  mh-infprim2bi  36904  eleq2w2ALT  37529  bj-idres  37649  mptsnunlem  37829  wl-dfcleq  38005  wl-dfclel  38006  ptrest  38115  poimirlem25  38141  mblfinlem2  38154  mblfinlem3  38155  mblfinlem4  38156  ismblfin  38157  mbfposadd  38163  itg2addnclem  38167  ftc1anclem5  38193  ftc1anclem6  38194  ftc1anclem7  38195  ftc1anc  38197  areacirclem5  38208  fdc1  38242  inxprnres  38794  fsumshftd  39573  pmapglb  40391  polval2N  40527  osumcllem4N  40580  pexmidlem1N  40591  dih1dimatlem  41950  mapdh9a  42410  mapdh9aOLDN  42411  sticksstones2  42761  fsuppind  43169  fphpd  43390  fphpdo  43391  pellex  43409  setindtrs  43599  dford3lem2  43601  fnwe2lem2  43625  mendlmod  43763  cantnfub  43895  tfsconcat0i  43919  rababg  44147  fsovrfovd  44582  fsovcnvlem  44586  scottabf  44813  trfr  45535  elunif  45593  iunincfi  45669  cbvmpo2  45672  cbvmpo1  45673  disjf1  45758  wessf1ornlem  45760  disjinfi  45767  supxrleubrnmptf  46022  monoordxr  46053  monoord2xr  46055  fsummulc1f  46144  fsumnncl  46145  fsumf1of  46147  fsumiunss  46148  fsumreclf  46149  fsumlessf  46150  fsumsermpt  46152  fmulcl  46154  fmul01lt1lem2  46158  fprodexp  46167  fprodabs2  46168  climmulf  46177  climexp  46178  climrecf  46182  climinff  46184  climaddf  46188  mullimc  46189  limcperiod  46201  sumnnodd  46203  neglimc  46218  addlimc  46219  climsubmpt  46231  climreclf  46235  climeldmeqmpt  46239  climfveqmpt  46242  fnlimfvre  46245  climfveqf  46251  climfveqmpt3  46253  climeldmeqf  46254  climeqf  46259  climeldmeqmpt3  46260  climinf2  46278  limsupequz  46294  limsupequzmptf  46302  lmbr3  46318  cnrefiisp  46401  cncfshift  46445  fprodcncf  46471  dvmptmulf  46508  dvmptfprod  46516  dvnprodlem1  46517  dvnprodlem3  46519  stoweidlem16  46587  stoweidlem34  46605  stoweidlem62  46633  dirkercncflem2  46675  fourierdlem12  46690  fourierdlem15  46693  fourierdlem34  46712  fourierdlem50  46727  fourierdlem73  46750  fourierdlem94  46771  fourierdlem112  46789  fourierdlem113  46790  intsaluni  46900  sge0lempt  46981  sge0iunmptlemfi  46984  sge0iunmptlemre  46986  sge0iunmpt  46989  sge0ltfirpmpt2  46997  sge0isummpt2  47003  sge0xaddlem2  47005  sge0xadd  47006  meadjiun  47037  voliunsge0lem  47043  meaiuninclem  47051  meaiunincf  47054  meaiuninc3v  47055  meaiuninc3  47056  meaiininclem  47057  meaiininc  47058  isomennd  47102  ovn0lem  47136  sge0hsphoire  47160  hoidmvlelem1  47166  hoidmvlelem2  47167  hoidmvlelem3  47168  hoidmvlelem5  47170  hspmbllem2  47198  hoimbl2  47236  vonhoire  47243  vonioo  47253  vonicc  47256  vonn0ioo2  47261  vonn0icc2  47263  pimincfltioc  47287  salpreimagtlt  47301  smflimlem4  47345  ormkglobd  47448  sinnpoly  47482  rexrsb  47691  ichexmpl2  48073  ichnreuop  48075  sbgoldbm  48403  bgoldbnnsum3prm  48423  tgoldbach  48436  srhmsubcALTV  48944  cbvmpox2  48955  mo0sn  49434  f1omoOLD  49512  isthincd2lem1  50043  thincmo  50046  euendfunc  50144