Theorem eleq1w 2845

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

Note that this provides a proof of ax-8 2147 from Tarski's FOL and dfclel 2838 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 232), 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 2059	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 643	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1954	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		dfclel 2838	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		dfclel 2838	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2837

This theorem is used by:  clelsb1  2889  cleqh  2891  nfcjust  2910  nfcr  2914  cleqf  2952  rspw  3241  cbvralvw  3242  cbvrexvw  3243  cbvralfw  3304  cbvralsvw  3315  cbvralf  3347  ralcom2  3364  moel  3387  cbvrmovw  3388  cbvreuvw  3389  cbvrmow  3392  cbvreu  3406  cbvrabv  3424  rabrabi  3433  cbvrabw  3449  nfrab  3451  cbvrab  3452  elrab2w  3653  reu2  3686  reu6  3687  rmo4  3691  reu8  3694  2reu5  3719  csbied  3886  difjust  3904  unjust  3906  injust  3908  dfss2  3920  dfssf  3925  eqeuel  4316  rabeq0w  4340  disj  4406  reldisj  4409  ralidmw  4475  dfif6  4488  rabsnifsb  4686  eluniab  4884  unissb  4904  uniintsn  4948  dfiun2g  4992  dfiunv2  4996  disjxun  5105  cbvmptf  5209  cbvmptfg  5210  cbvmptv  5213  dftr2c  5219  isso2i  5604  dfres2  6041  imai  6074  frpoinsg  6345  tz7.7  6387  fvn0ssdmfun  7070  fmptco  7126  cbvriotaw  7382  cbvriotavw  7383  cbvriota  7386  cbvmpox  7509  cbvmpov  7511  tfis  7854  tfindes  7862  peano5  7893  findes  7900  dfoprab4f  8056  fmpox  8067  xpord2indlem  8148  poseq  8159  soseq  8160  smogt  8359  resixpfo  8946  ixpsnf1o  8948  dom2lem  9001  mapsnend  9046  pw2f1olem  9082  pssnn  9166  ssfi  9170  findcard3  9256  ordiso2  9490  elirrvOLDOLD  9574  cantnflem1d  9670  cantnf  9675  setind  9729  frinsg  9736  tz9.12lem3  9774  scottabf  9881  infxpen  10020  dfac5lem4  10132  dfac12lem2  10150  kmlem14  10169  cfsmolem  10275  sornom  10282  isf32lem9  10366  axdc2  10454  fpwwe2lem7  10649  fpwwe2  10655  wunex2  10750  dedekindle  11401  wloglei  11773  uzind4s  12960  seqof2  14126  reuccatpfxs1  14818  shftfn  15148  rexuz3  15438  zsum  15806  fsum  15808  sumss  15812  sumss2  15814  fsumcvg2  15815  fsumser  15818  fsumclf  15826  fsumsplitf  15830  isumless  15936  prodfdiv  15987  cbvprod  16004  cbvprodv  16005  zprod  16028  fprod  16032  fprodntriv  16033  prodss  16038  fprod2dlem  16071  fproddivf  16078  fprodsplitf  16079  rpnnen2lem10  16315  cpnnen  16321  sumeven  16481  sumodd  16482  sadcp1  16549  smupp1  16574  pcmptdvds  16990  prmreclem2  17013  prmreclem5  17016  prmreclem6  17017  prmrec  17018  prmdvdsprmo  17138  iscatd2  17773  initoeu2  18109  yoniso  18377  sgrpidmnd  18845  mndind  18941  eqg0subg  19328  symggen  19601  dprd2d2  20177  srhmsubc  20846  isdrngrd  20936  isdrngrdOLD  20938  lbspss  21270  frlmphl  21998  frlmup1  22015  opsrtoslem1  22275  selvvvval  22362  mdetralt  22834  mdetralt2  22835  mdetunilem2  22839  maducoeval2  22866  chfacfscmulgsum  23089  chfacfpmmulgsum  23093  isclo2  23317  neiptopnei  23361  ptcldmpt  23844  elmptrab  24057  hausflimi  24210  hausflim  24211  alexsubALTlem3  24279  alexsubALTlem4  24280  ptcmplem2  24283  cnextcn  24297  cnextfres1  24298  tgphaus  24347  ustuqtop  24476  utopsnneip  24478  ucncn  24514  nrmmetd  24804  xrhmeo  25178  iscau2  25509  caucfil  25515  cmetcaulem  25520  bcth  25561  vitalilem3  25842  vitali  25845  i1f1lem  25921  itg11  25923  i1fres  25937  mbfi1fseq  25953  mbfi1flim  25955  itg2uba  25975  itg2splitlem  25980  isibl2  25998  cbvitg  26008  cbvitgv  26009  itgss3  26047  dvmptfsum  26207  rolle  26222  elply2  26426  plyexmo  26547  lgamgulmlem2  27267  prmorcht  27415  pclogsum  27452  dchr1  27494  lgsdir  27569  lgsdilem2  27570  lgsdi  27571  lgsne0  27572  lgsquadlem3  27619  lgsquad  27620  2sqlem8  27663  nosupcbv  27939  nosupno  27940  nosupdm  27941  nosupbnd1lem1  27945  noinfcbv  27954  noinfno  27955  noinfdm  27956  nocvxminlem  28020  legval  28927  legov  28928  tglineintmo  28990  tglowdim2ln  29000  ishpg  29117  lnopp2hpgb  29121  hpgerlem  29123  colopp  29127  elplngid  29140  lnincplng  29142  plngcp  29144  plngrot  29148  nhpmirhp  29156  lnperpexs  29190  ragraghl  29226  tgaaddcpbllem2  29230  tgaaddcpbllem3  29231  prlnghpg  29304  prlngmo  29312  tgaltai  29325  axcontlem1  29422  numedglnl  29602  uvtxnbgrvtx  29854  cusgrres  29909  wspniunwspnon  30392  rusgrnumwwlkb0  30443  frgr3vlem2  30755  3vfriswmgrlem  30758  fusgr2wsp2nb  30815  numclwlk2lem2f1o  30860  lpni  30962  pjhthmo  31784  chscllem2  32120  cbvdisjf  33046  2ndresdju  33124  fmptcof2  33132  aciunf1lem  33137  funcnv4mpt  33143  suppovss  33155  fpwrelmapffslem  33205  fsumiunle  33301  gsumwrd2dccatlem  33519  elrspunsn  33859  1arithufdlem3  33958  fedgmullem1  34141  fldextrspunlsp  34186  extdgfialglem2  34205  zarclssn  34385  esumcvg  34598  fiunelros  34687  measiun  34731  bnj1146  35302  bnj1185  35304  bnj1385  35343  bnj1014  35472  bnj1112  35494  bnj1123  35497  bnj1228  35522  bnj1326  35537  bnj1321  35538  bnj1384  35543  bnj1417  35552  bnj1497  35571  trssfir1om  35623  r1omhfb  35624  fineqvnttrclse  35652  axregscl  35656  setindregs  35658  trssfir1omregs  35664  r1omhfbregs  35665  onvf1odlem2  35703  onvf1odlem3  35704  gonarlem  35975  goalrlem  35977  goalr  35978  mrsubrn  36094  dfon2lem6  36367  dfbigcup2  36478  lineintmo  36739  cbvralvw2  36848  cbvrexvw2  36849  cbvrmovw2  36850  cbvreuvw2  36851  cbvmptvw2  36856  cbvprodvw2  36869  cbvrmodavw  36874  cbvreudavw  36875  cbvrabdavw  36883  cbvmptdavw  36889  cbvriotadavw  36892  cbvixpdavw  36900  cbvproddavw  36902  cbvitgdavw  36903  cbvrabdavw2  36907  cbvmptdavw2  36910  cbvriotadavw2  36912  weiunlem  37084  dfttc4  37151  mh-infprim2bi  37168  eleq2w2ALT  37793  bj-idres  37914  mptsnunlem  38094  wl-dfcleq  38270  wl-dfclel  38271  ptrest  38370  poimirlem25  38396  mblfinlem2  38409  mblfinlem3  38410  mblfinlem4  38411  ismblfin  38412  mbfposadd  38418  itg2addnclem  38422  ftc1anclem5  38448  ftc1anclem6  38449  ftc1anclem7  38450  ftc1anc  38452  areacirclem5  38463  fdc1  38498  inxprnres  39048  fsumshftd  39827  pmapglb  40645  polval2N  40781  osumcllem4N  40834  pexmidlem1N  40845  dih1dimatlem  42204  mapdh9a  42664  mapdh9aOLDN  42665  sticksstones2  43015  fsuppind  43438  fphpd  43659  fphpdo  43660  pellex  43678  setindtrs  43868  dford3lem2  43870  fnwe2lem2  43894  mendlmod  44032  cantnfub  44164  tfsconcat0i  44188  rababg  44416  fsovrfovd  44851  fsovcnvlem  44855  trfr  45787  elunif  45852  iunincfi  45928  cbvmpo2  45931  cbvmpo1  45932  disjf1  46017  wessf1ornlem  46019  disjinfi  46026  supxrleubrnmptf  46281  monoordxr  46312  monoord2xr  46314  fsummulc1f  46403  fsumnncl  46404  fsumf1of  46406  fsumiunss  46407  fsumreclf  46408  fsumlessf  46409  fsumsermpt  46411  fmulcl  46413  fmul01lt1lem2  46417  fprodexp  46426  fprodabs2  46427  climmulf  46436  climexp  46437  climrecf  46441  climinff  46443  climaddf  46447  mullimc  46448  limcperiod  46460  sumnnodd  46462  neglimc  46477  addlimc  46478  climsubmpt  46490  climreclf  46494  climeldmeqmpt  46498  climfveqmpt  46501  fnlimfvre  46504  climfveqf  46510  climfveqmpt3  46512  climeldmeqf  46513  climeqf  46518  climeldmeqmpt3  46519  climinf2  46537  limsupequz  46553  limsupequzmptf  46561  lmbr3  46577  cnrefiisp  46660  cncfshift  46704  fprodcncf  46730  dvmptmulf  46767  dvmptfprod  46775  dvnprodlem1  46776  dvnprodlem3  46778  stoweidlem16  46846  stoweidlem34  46864  stoweidlem62  46892  dirkercncflem2  46934  fourierdlem12  46949  fourierdlem15  46952  fourierdlem34  46971  fourierdlem50  46986  fourierdlem73  47009  fourierdlem94  47030  fourierdlem112  47048  fourierdlem113  47049  intsaluni  47159  sge0lempt  47240  sge0iunmptlemfi  47243  sge0iunmptlemre  47245  sge0iunmpt  47248  sge0ltfirpmpt2  47256  sge0isummpt2  47262  sge0xaddlem2  47264  sge0xadd  47265  meadjiun  47296  voliunsge0lem  47302  meaiuninclem  47310  meaiunincf  47313  meaiuninc3v  47314  meaiuninc3  47315  meaiininclem  47316  meaiininc  47317  isomennd  47361  ovn0lem  47395  sge0hsphoire  47419  hoidmvlelem1  47425  hoidmvlelem2  47426  hoidmvlelem3  47427  hoidmvlelem5  47429  hspmbllem2  47457  hoimbl2  47495  vonhoire  47502  vonioo  47512  vonicc  47515  vonn0ioo2  47520  vonn0icc2  47522  pimincfltioc  47546  salpreimagtlt  47560  smflimlem4  47604  ormkglobd  47707  sinnpoly  47761  rexrsb  47990  ichexmpl2  48372  ichnreuop  48374  sbgoldbm  48702  bgoldbnnsum3prm  48722  tgoldbach  48735  srhmsubcALTV  49242  cbvmpox2  49268  mo0sn  49746  f1omoOLD  49822  isthincd2lem1  50353  thincmo  50356  euendfunc  50454