Theorem wel 2210

Description: Extend wff definition to include atomic formulas with the membership predicate. This is read either "𝑥 is an element of 𝑦", or "𝑥 is a member of 𝑦", or "𝑥 belongs to 𝑦", or "𝑦 contains 𝑥". Note: The phrase "𝑦 includes 𝑥 " means "𝑥 is a subset of 𝑦"; to use it also for 𝑥 ∈ 𝑦, as some authors occasionally do, is poor form and causes confusion, according to George Boolos (1992 lecture at MIT).

This syntactical construction introduces a binary non-logical predicate symbol ∈ into our predicate calculus. We will eventually use it for the membership predicate of set theory, but that is irrelevant at this point: the predicate calculus axioms for ∈ apply to any arbitrary binary predicate symbol. "Non-logical" means that the predicate is presumed to have additional properties beyond the realm of predicate calculus, although these additional properties are not specified by predicate calculus itself but rather by the axioms of a theory (in our case set theory) added to predicate calculus. "Binary" means that the predicate has two arguments.

Instead of introducing wel 2210 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wcel 2209. This lets us avoid overloading the ∈ connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2210 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2209. Note: To see the proof steps of this syntax proof, type "MM> SHOW PROOF wel / ALL" in the Metamath program. (Contributed by NM, 24-Jan-2006.)

Assertion

Ref	Expression
wel	wff 𝑥 ∈ 𝑦

Proof of Theorem wel

Step	Hyp	Ref	Expression
1		wcel 2209	1 wff 𝑥 ∈ 𝑦

This proof depends on syntax axioms:   ∈ wcel 2209

This theorem is used by:  elequ1  2213  elequ2  2214  cleljust  2215  elsb1  2216  elsb2  2217  dveel1  2218  dveel2  2219  axext3  2221  axext4  2222  bm1.1  2223  ru  3050  nfuni  3941  nfunid  3942  unieq  3944  inteq  3973  nfint  3980  uniiun  4066  intiin  4067  trint  4244  axsepg  4250  sepg  4251  sepgi  4252  bm1.3ii  4254  zfnuleu  4257  0ex  4260  nalset  4263  vnex  4264  repizf2  4299  axpweq  4308  zfpow  4312  axpow2  4313  axpow3  4314  el  4315  vpwex  4316  dtruarb  4328  exmidn0m  4338  exmidsssn  4339  fr0  4496  wetrep  4505  zfun  4579  axun2  4580  uniex2  4581  uniuni  4597  regexmid  4682  zfregfr  4721  ordwe  4723  wessep  4725  nnregexmid  4768  rele  4910  funimaexglem  5464  acexmidlem2  6082  acexmid  6084  dfsmo2  6558  smores2  6565  tfrcllemsucaccv  6625  pw2f1odclem  7134  findcard2d  7195  sspw1or2  7544  exmidfodomr  7556  acfun  7563  exmidontriimlem3  7579  exmidontriimlem4  7580  exmidontriim  7581  onntri13  7597  exmidontri  7598  onntri51  7599  onntri3or  7604  exmidmotap  7627  ccfunen  7630  cc1  7631  ltsopi  7687  fnn0nninf  10888  hashfibclem  11296  fsum2dlemstep  12217  fprod2dlemstep  12405  exmidunben  13366  prdsex  14221  isbasis3g  15196  tgcl  15214  tgss2  15229  blbas  15583  metrest  15656  dvmptfsum  15875  uhgrfm  16412  ushgrfm  16413  uhgrss  16414  uhgreq12g  16415  uhgrfun  16416  ushgruhgr  16419  isuhgropm  16420  uhgr0e  16421  uhgr0vb  16423  uhgr0  16424  uhgrun  16425  bdcuni  17000  bdcint  17001  bdcriota  17007  bdsep1  17009  bdsep2  17010  bdsepnft  17011  bdsepnf  17012  bdsepnfALT  17013  bdsepg  17014  bdbm1.3ii  17015  bj-axemptylem  17016  bj-axempty  17017  bj-axempty2  17018  bj-nalset  17019  bdinex1  17023  bj-zfpair2  17034  bj-axun2  17039  bj-uniex2  17040  bj-d0clsepcl  17049  bj-nn0suc0  17074  bj-nntrans  17075  bj-omex2  17101  strcollnft  17108  sscoll2  17112  nninfsellemcl  17152  nninfsellemsuc  17153  nninfsellemqall  17156  nninfomni  17160  exmidsbthrlem  17165