Theorem eleq1w 2808

Description: Weaker version of eleq1 2813 (but more general than elequ1 2105) not depending on ax-ext 2695 nor df-cleq 2716.

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∃wex 1773   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-clel 2802

This theorem is referenced by:  clelsb1  2852  cleqh  2855  nfcjust  2876  nfcr  2880  nfcriOLD  2885  nfcriOLDOLD  2886  cleqf  2926  rspw  3225  cbvralvw  3226  cbvrexvw  3227  cbvralfw  3293  cbvralfwOLD  3312  cbvralf  3348  ralcom2  3365  moel  3390  cbvrmovw  3391  cbvreuvw  3392  moelOLD  3393  cbvrmow  3397  cbvreuwOLD  3404  cbvreu  3416  cbvrabv  3434  rabrabi  3442  cbvrabw  3459  nfrab  3464  cbvrab  3465  reu2  3714  reu6  3715  rmo4  3719  reu8  3722  2reu5  3747  ru  3769  csbied  3924  difjust  3943  unjust  3945  injust  3947  dfss2f  3965  dfdif3  4107  eqeuel  4355  rabeq0w  4376  disj  4440  reldisj  4444  ralidmw  4500  dfif6  4524  rabsnifsb  4719  eluniab  4914  unissb  4934  elintabOLD  4954  uniintsn  4982  dfiun2g  5024  dfiunv2  5029  disjxun  5137  cbvmptf  5248  cbvmptfg  5249  cbvmptv  5252  dftr2c  5259  isso2i  5614  dfres2  6032  imai  6064  frpoinsg  6335  wfisgOLD  6346  tz7.7  6381  fvn0ssdmfun  7067  fmptco  7120  cbvriotaw  7367  cbvriotavw  7368  cbvriota  7372  cbvmpox  7495  tfis  7838  tfindes  7846  peano5  7878  findes  7887  dfoprab4f  8036  fmpox  8047  xpord2indlem  8128  poseq  8139  soseq  8140  wfrlem10OLD  8314  smogt  8363  resixpfo  8927  ixpsnf1o  8929  dom2lem  8985  mapsnend  9033  pw2f1olem  9073  pssnn  9165  ssfi  9170  findcard3  9282  findcard3OLD  9283  ordiso2  9507  elirrv  9588  cantnflem1d  9680  cantnf  9685  setind  9726  frinsg  9743  tz9.12lem3  9781  infxpen  10006  dfac12lem2  10136  kmlem14  10155  cfsmolem  10262  sornom  10269  isf32lem9  10353  axdc2  10441  fpwwe2lem7  10629  fpwwe2  10635  wunex2  10730  dedekindle  11376  wloglei  11744  uzind4s  12890  seqof2  14024  reuccatpfxs1  14695  shftfn  15018  rexuz3  15293  zsum  15662  fsum  15664  sumss  15668  sumss2  15670  fsumcvg2  15671  fsumser  15674  fsumclf  15682  fsumsplitf  15686  isumless  15789  prodfdiv  15840  cbvprod  15857  zprod  15879  fprod  15883  fprodntriv  15884  prodss  15889  fprod2dlem  15922  fproddivf  15929  fprodsplitf  15930  rpnnen2lem10  16165  cpnnen  16171  sumeven  16329  sumodd  16330  sadcp1  16395  smupp1  16420  pcmptdvds  16828  prmreclem2  16851  prmreclem5  16854  prmreclem6  16855  prmrec  16856  prmdvdsprmo  16976  iscatd2  17626  initoeu2  17970  yoniso  18242  sgrpidmnd  18664  mndind  18745  eqg0subg  19114  symggen  19382  dprd2d2  19958  srhmsubc  20568  isdrngrd  20613  isdrngrdOLD  20615  lbspss  20922  frlmphl  21646  frlmup1  21663  opsrtoslem1  21928  mdetralt  22434  mdetralt2  22435  mdetunilem2  22439  maducoeval2  22466  chfacfscmulgsum  22686  chfacfpmmulgsum  22690  isclo2  22916  neiptopnei  22960  ptcldmpt  23442  elmptrab  23655  hausflimi  23808  hausflim  23809  alexsubALTlem3  23877  alexsubALTlem4  23878  ptcmplem2  23881  cnextcn  23895  cnextfres1  23896  tgphaus  23945  ustuqtop  24075  utopsnneip  24077  ucncn  24114  nrmmetd  24407  xrhmeo  24795  iscau2  25129  caucfil  25135  cmetcaulem  25140  bcth  25181  vitalilem3  25463  vitali  25466  i1f1lem  25542  itg11  25544  i1fres  25559  mbfi1fseq  25575  mbfi1flim  25577  itg2uba  25597  itg2splitlem  25602  isibl2  25620  cbvitg  25629  itgss3  25668  dvmptfsum  25831  rolle  25846  elply2  26052  plyexmo  26169  lgamgulmlem2  26881  prmorcht  27029  pclogsum  27067  dchr1  27109  lgsdir  27184  lgsdilem2  27185  lgsdi  27186  lgsne0  27187  lgsquadlem3  27234  lgsquad  27235  2sqlem8  27278  nosupcbv  27554  nosupno  27555  nosupdm  27556  nosupbnd1lem1  27560  noinfcbv  27569  noinfno  27570  noinfdm  27571  nocvxminlem  27629  legval  28307  legov  28308  tglineintmo  28365  tglowdim2ln  28374  ishpg  28482  lnopp2hpgb  28486  hpgerlem  28488  colopp  28492  axcontlem1  28694  numedglnl  28876  uvtxnbgrvtx  29122  cusgrres  29177  wspniunwspnon  29649  rusgrnumwwlkb0  29697  frgr3vlem2  29999  3vfriswmgrlem  30002  fusgr2wsp2nb  30059  numclwlk2lem2f1o  30104  lpni  30205  pjhthmo  31027  chscllem2  31363  cbvdisjf  32274  2ndresdju  32346  fmptcof2  32354  aciunf1lem  32359  funcnv4mpt  32366  suppovss  32378  fpwrelmapffslem  32429  fsumiunle  32505  elrspunsn  33019  fedgmullem1  33196  zarclssn  33345  esumcvg  33576  fiunelros  33664  measiun  33708  bnj1146  34293  bnj1185  34295  bnj1385  34334  bnj1014  34463  bnj1112  34485  bnj1123  34488  bnj1228  34513  bnj1326  34528  bnj1321  34529  bnj1384  34534  bnj1417  34543  bnj1497  34562  gonarlem  34876  goalrlem  34878  goalr  34879  mrsubrn  34995  dfon2lem6  35256  dfbigcup2  35367  lineintmo  35625  eleq2w2ALT  36419  bj-idres  36532  mptsnunlem  36710  ptrest  36981  poimirlem25  37007  mblfinlem2  37020  mblfinlem3  37021  mblfinlem4  37022  ismblfin  37023  mbfposadd  37029  itg2addnclem  37033  ftc1anclem5  37059  ftc1anclem6  37060  ftc1anclem7  37061  ftc1anc  37063  areacirclem5  37074  fdc1  37108  inxprnres  37655  fsumshftd  38316  pmapglb  39135  polval2N  39271  osumcllem4N  39324  pexmidlem1N  39335  dih1dimatlem  40694  mapdh9a  41154  mapdh9aOLDN  41155  sticksstones2  41460  selvvvval  41650  fsuppind  41655  elrab2w  41924  fphpd  42068  fphpdo  42069  pellex  42087  setindtrs  42278  dford3lem2  42280  fnwe2lem2  42307  mendlmod  42449  cantnfub  42585  tfsconcat0i  42609  rababg  42839  fsovrfovd  43274  fsovcnvlem  43278  scottabf  43513  elunif  44214  iunincfi  44296  cbvmpo2  44299  cbvmpo1  44300  disjf1  44392  wessf1ornlem  44394  disjinfi  44401  supxrleubrnmptf  44671  monoordxr  44703  monoord2xr  44705  fsummulc1f  44797  fsumnncl  44798  fsumf1of  44800  fsumiunss  44801  fsumreclf  44802  fsumlessf  44803  fsumsermpt  44805  fmulcl  44807  fmul01lt1lem2  44811  fprodexp  44820  fprodabs2  44821  climmulf  44830  climexp  44831  climrecf  44835  climinff  44837  climaddf  44841  mullimc  44842  limcperiod  44854  sumnnodd  44856  neglimc  44873  addlimc  44874  climsubmpt  44886  climreclf  44890  climeldmeqmpt  44894  climfveqmpt  44897  fnlimfvre  44900  climfveqf  44906  climfveqmpt3  44908  climeldmeqf  44909  climeqf  44914  climeldmeqmpt3  44915  climinf2  44933  limsupequz  44949  limsupequzmptf  44957  lmbr3  44973  cnrefiisp  45056  cncfshift  45100  fprodcncf  45126  dvmptmulf  45163  dvmptfprod  45171  dvnprodlem1  45172  dvnprodlem3  45174  stoweidlem16  45242  stoweidlem34  45260  stoweidlem62  45288  dirkercncflem2  45330  fourierdlem12  45345  fourierdlem15  45348  fourierdlem34  45367  fourierdlem50  45382  fourierdlem73  45405  fourierdlem94  45426  fourierdlem112  45444  fourierdlem113  45445  intsaluni  45555  sge0lempt  45636  sge0iunmptlemfi  45639  sge0iunmptlemre  45641  sge0iunmpt  45644  sge0ltfirpmpt2  45652  sge0isummpt2  45658  sge0xaddlem2  45660  sge0xadd  45661  meadjiun  45692  voliunsge0lem  45698  meaiuninclem  45706  meaiunincf  45709  meaiuninc3v  45710  meaiuninc3  45711  meaiininclem  45712  meaiininc  45713  isomennd  45757  ovn0lem  45791  sge0hsphoire  45815  hoidmvlelem1  45821  hoidmvlelem2  45822  hoidmvlelem3  45823  hoidmvlelem5  45825  hspmbllem2  45853  hoimbl2  45891  vonhoire  45898  vonioo  45908  vonicc  45911  vonn0ioo2  45916  vonn0icc2  45918  pimincfltioc  45942  salpreimagtlt  45956  smflimlem4  46000  rexrsb  46318  ichexmpl2  46648  ichnreuop  46650  sbgoldbm  46962  bgoldbnnsum3prm  46982  tgoldbach  46995  srhmsubcALTV  47213  cbvmpox2  47225  mo0sn  47712  f1omo  47739  isthincd2lem1  47859  thincmo  47861