Theorem wel 2177

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 2177 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 2176. This lets us avoid overloading the ∈ connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2177 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2176. 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 2176	1 wff 𝑥 ∈ 𝑦

Syntax hints:   ∈ wcel 2176

This theorem is referenced by:  elequ1  2180  elequ2  2181  cleljust  2182  elsb1  2183  elsb2  2184  dveel1  2185  dveel2  2186  axext3  2188  axext4  2189  bm1.1  2190  ru  2997  nfuni  3856  nfunid  3857  unieq  3859  inteq  3888  nfint  3895  uniiun  3981  intiin  3982  trint  4157  axsep2  4163  bm1.3ii  4165  zfnuleu  4168  0ex  4171  nalset  4174  vnex  4175  repizf2  4206  axpweq  4215  zfpow  4219  axpow2  4220  axpow3  4221  el  4222  vpwex  4223  dtruarb  4235  exmidn0m  4245  exmidsssn  4246  fr0  4398  wetrep  4407  zfun  4481  axun2  4482  uniuni  4498  regexmid  4583  zfregfr  4622  ordwe  4624  wessep  4626  nnregexmid  4669  rele  4808  funimaexglem  5357  acexmidlem2  5941  acexmid  5943  dfsmo2  6373  smores2  6380  tfrcllemsucaccv  6440  pw2f1odclem  6931  findcard2d  6988  exmidfodomr  7312  acfun  7319  exmidontriimlem3  7335  exmidontriimlem4  7336  exmidontriim  7337  onntri13  7350  exmidontri  7351  onntri51  7352  onntri3or  7357  exmidmotap  7373  ccfunen  7376  cc1  7377  ltsopi  7433  fnn0nninf  10583  fsum2dlemstep  11745  fprod2dlemstep  11933  exmidunben  12797  prdsex  13101  isbasis3g  14518  tgcl  14536  tgss2  14551  blbas  14905  metrest  14978  dvmptfsum  15197  bdcuni  15812  bdcint  15813  bdcriota  15819  bdsep1  15821  bdsep2  15822  bdsepnft  15823  bdsepnf  15824  bdsepnfALT  15825  bdzfauscl  15826  bdbm1.3ii  15827  bj-axemptylem  15828  bj-axempty  15829  bj-axempty2  15830  bj-nalset  15831  bdinex1  15835  bj-zfpair2  15846  bj-axun2  15851  bj-uniex2  15852  bj-d0clsepcl  15861  bj-nn0suc0  15886  bj-nntrans  15887  bj-omex2  15913  strcollnft  15920  sscoll2  15924  nninfsellemcl  15948  nninfsellemsuc  15949  nninfsellemqall  15952  nninfomni  15956  exmidsbthrlem  15961