Theorem eleq1w 2821

Description: Weaker version of eleq1 2826 (but more general than elequ1 2115) not depending on ax-ext 2709 nor df-cleq 2730.

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817

This theorem is referenced by:  cleqh  2862  clelsb1  2866  nfcjust  2887  nfcr  2891  nfcriOLD  2896  nfcriOLDOLD  2897  cleqf  2937  rspw  3128  ralcom2  3288  nfrab  3312  moel  3349  cbvralfw  3358  cbvralfwOLD  3359  cbvralf  3361  cbvreuw  3365  cbvrmow  3366  cbvreu  3370  cbvralvw  3372  cbvrexvw  3373  cbvrmovw  3374  cbvreuvw  3375  cbvrabw  3414  cbvrab  3415  cbvrabv  3416  rabrabi  3417  ralab2OLD  3628  rexab2OLD  3631  reu2  3655  reu6  3656  rmo4  3660  reu8  3663  2reu5  3688  ru  3710  csbied  3866  difjust  3885  unjust  3887  injust  3889  dfss2f  3907  dfdif3  4045  eqeuel  4293  rabeq0w  4314  disj  4378  reldisj  4382  ralidmw  4435  dfif6  4459  rabsnifsb  4655  eluniab  4851  elintab  4887  uniintsn  4915  dfiunv2  4961  disjxun  5068  cbvmptf  5179  cbvmptfg  5180  cbvmptv  5183  isso2i  5529  dfres2  5938  imai  5971  frpoinsg  6231  wfisgOLD  6242  tz7.7  6277  fvn0ssdmfun  6934  fmptco  6983  cbvriotaw  7221  cbvriotavw  7222  cbvriota  7226  cbvmpox  7346  tfis  7676  tfindes  7684  peano5  7714  findes  7723  dfoprab4f  7869  fmpox  7880  wfrlem10OLD  8120  smogt  8169  resixpfo  8682  ixpsnf1o  8684  dom2lem  8735  mapsnend  8780  pw2f1olem  8816  pssnn  8913  ssfi  8918  findcard3  8987  ordiso2  9204  elirrv  9285  cantnflem1d  9376  cantnf  9381  setind  9423  frinsg  9440  tz9.12lem3  9478  infxpen  9701  dfac12lem2  9831  kmlem14  9850  cfsmolem  9957  sornom  9964  isf32lem9  10048  axdc2  10136  fpwwe2lem7  10324  fpwwe2  10330  wunex2  10425  dedekindle  11069  wloglei  11437  uzind4s  12577  seqof2  13709  reuccatpfxs1  14388  shftfn  14712  rexuz3  14988  zsum  15358  fsum  15360  sumss  15364  sumss2  15366  fsumcvg2  15367  fsumser  15370  fsumclf  15378  fsumsplitf  15382  isumless  15485  prodfdiv  15536  cbvprod  15553  zprod  15575  fprod  15579  fprodntriv  15580  prodss  15585  fprod2dlem  15618  fproddivf  15625  fprodsplitf  15626  rpnnen2lem10  15860  cpnnen  15866  sumeven  16024  sumodd  16025  sadcp1  16090  smupp1  16115  pcmptdvds  16523  prmreclem2  16546  prmreclem5  16549  prmreclem6  16550  prmrec  16551  prmdvdsprmo  16671  iscatd2  17307  initoeu2  17647  yoniso  17919  sgrpidmnd  18305  mndind  18381  symggen  18993  dprd2d2  19562  isdrngrd  19932  lbspss  20259  frlmphl  20898  frlmup1  20915  opsrtoslem1  21172  mdetralt  21665  mdetralt2  21666  mdetunilem2  21670  maducoeval2  21697  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  isclo2  22147  neiptopnei  22191  ptcldmpt  22673  elmptrab  22886  hausflimi  23039  hausflim  23040  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem2  23112  cnextcn  23126  cnextfres1  23127  tgphaus  23176  ustuqtop  23306  utopsnneip  23308  ucncn  23345  nrmmetd  23636  xrhmeo  24015  iscau2  24346  caucfil  24352  cmetcaulem  24357  bcth  24398  vitalilem3  24679  vitali  24682  i1f1lem  24758  itg11  24760  i1fres  24775  mbfi1fseq  24791  mbfi1flim  24793  itg2uba  24813  itg2splitlem  24818  isibl2  24836  cbvitg  24845  itgss3  24884  dvmptfsum  25044  rolle  25059  elply2  25262  plyexmo  25378  lgamgulmlem2  26084  prmorcht  26232  pclogsum  26268  dchr1  26310  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  lgsquadlem3  26435  lgsquad  26436  2sqlem8  26479  legval  26849  legov  26850  tglineintmo  26907  tglowdim2ln  26916  ishpg  27024  lnopp2hpgb  27028  hpgerlem  27030  colopp  27034  axcontlem1  27235  numedglnl  27417  uvtxnbgrvtx  27663  cusgrres  27718  wspniunwspnon  28189  rusgrnumwwlkb0  28237  frgr3vlem2  28539  3vfriswmgrlem  28542  fusgr2wsp2nb  28599  numclwlk2lem2f1o  28644  lpni  28743  pjhthmo  29565  chscllem2  29901  cbvdisjf  30811  2ndresdju  30887  fmptcof2  30896  aciunf1lem  30901  funcnv4mpt  30908  suppovss  30919  fpwrelmapffslem  30969  fsumiunle  31045  fedgmullem1  31612  zarclssn  31725  esumcvg  31954  fiunelros  32042  measiun  32086  bnj1146  32671  bnj1185  32673  bnj1385  32712  bnj1014  32841  bnj1112  32863  bnj1123  32866  bnj1228  32891  bnj1326  32906  bnj1321  32907  bnj1384  32912  bnj1417  32921  bnj1497  32940  gonarlem  33256  goalrlem  33258  goalr  33259  mrsubrn  33375  dfon2lem6  33670  xpord2ind  33721  xpord3ind  33727  poseq  33729  soseq  33730  nosupcbv  33832  nosupno  33833  nosupdm  33834  nosupbnd1lem1  33838  noinfcbv  33847  noinfno  33848  noinfdm  33849  nocvxminlem  33899  dfbigcup2  34128  lineintmo  34386  eleq2w2ALT  35147  bj-idres  35258  mptsnunlem  35436  ptrest  35703  poimirlem25  35729  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  mbfposadd  35751  itg2addnclem  35755  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anc  35785  areacirclem5  35796  fdc1  35831  inxprnres  36354  fsumshftd  36893  pmapglb  37711  polval2N  37847  osumcllem4N  37900  pexmidlem1N  37911  dih1dimatlem  39270  mapdh9a  39730  mapdh9aOLDN  39731  sticksstones2  40031  elrab2w  40095  fsuppind  40202  fphpd  40554  fphpdo  40555  pellex  40573  setindtrs  40763  dford3lem2  40765  fnwe2lem2  40792  mendlmod  40934  rababg  41070  fsovrfovd  41506  fsovcnvlem  41510  scottabf  41747  elunif  42448  iunincfi  42533  cbvmpo2  42536  cbvmpo1  42537  disjf1  42609  wessf1ornlem  42611  disjinfi  42620  supxrleubrnmptf  42881  monoordxr  42913  monoord2xr  42915  fsummulc1f  43002  fsumnncl  43003  fsumf1of  43005  fsumiunss  43006  fsumreclf  43007  fsumlessf  43008  fsumsermpt  43010  fmulcl  43012  fmul01lt1lem2  43016  fprodexp  43025  fprodabs2  43026  climmulf  43035  climexp  43036  climrecf  43040  climinff  43042  climaddf  43046  mullimc  43047  limcperiod  43059  sumnnodd  43061  neglimc  43078  addlimc  43079  climsubmpt  43091  climreclf  43095  climeldmeqmpt  43099  climfveqmpt  43102  fnlimfvre  43105  climfveqf  43111  climfveqmpt3  43113  climeldmeqf  43114  climeqf  43119  climeldmeqmpt3  43120  climinf2  43138  limsupequz  43154  limsupequzmptf  43162  lmbr3  43178  cnrefiisp  43261  cncfshift  43305  fprodcncf  43331  dvmptmulf  43368  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem3  43379  stoweidlem16  43447  stoweidlem34  43465  stoweidlem62  43493  dirkercncflem2  43535  fourierdlem12  43550  fourierdlem15  43553  fourierdlem34  43572  fourierdlem50  43587  fourierdlem73  43610  fourierdlem94  43631  fourierdlem112  43649  fourierdlem113  43650  intsaluni  43758  sge0lempt  43838  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0ltfirpmpt2  43854  sge0isummpt2  43860  sge0xaddlem2  43862  sge0xadd  43863  meadjiun  43894  voliunsge0lem  43900  meaiuninclem  43908  meaiunincf  43911  meaiuninc3v  43912  meaiuninc3  43913  meaiininclem  43914  meaiininc  43915  isomennd  43959  ovn0lem  43993  sge0hsphoire  44017  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem5  44027  hspmbllem2  44055  hoimbl2  44093  vonhoire  44100  vonioo  44110  vonicc  44113  vonn0ioo2  44118  vonn0icc2  44120  pimincfltioc  44140  salpreimagtlt  44153  smflimlem4  44196  rexrsb  44479  ichexmpl2  44810  ichnreuop  44812  sbgoldbm  45124  bgoldbnnsum3prm  45144  tgoldbach  45157  srhmsubc  45522  srhmsubcALTV  45540  cbvmpox2  45559  mo0sn  46049  f1omo  46076  isthincd2lem1  46196  thincmo  46198