Theorem wel 2176

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

Syntax hints:   ∈ wcel 2175

This theorem is referenced by:  elequ1  2179  elequ2  2180  cleljust  2181  elsb1  2182  elsb2  2183  dveel1  2184  dveel2  2185  axext3  2187  axext4  2188  bm1.1  2189  ru  2996  nfuni  3855  nfunid  3856  unieq  3858  inteq  3887  nfint  3894  uniiun  3980  intiin  3981  trint  4156  axsep2  4162  bm1.3ii  4164  zfnuleu  4167  0ex  4170  nalset  4173  vnex  4174  repizf2  4205  axpweq  4214  zfpow  4218  axpow2  4219  axpow3  4220  el  4221  vpwex  4222  dtruarb  4234  exmidn0m  4244  exmidsssn  4245  fr0  4397  wetrep  4406  zfun  4480  axun2  4481  uniuni  4497  regexmid  4582  zfregfr  4621  ordwe  4623  wessep  4625  nnregexmid  4668  rele  4807  funimaexglem  5356  acexmidlem2  5940  acexmid  5942  dfsmo2  6372  smores2  6379  tfrcllemsucaccv  6439  pw2f1odclem  6930  findcard2d  6987  exmidfodomr  7311  acfun  7318  exmidontriimlem3  7334  exmidontriimlem4  7335  exmidontriim  7336  onntri13  7349  exmidontri  7350  onntri51  7351  onntri3or  7356  exmidmotap  7372  ccfunen  7375  cc1  7376  ltsopi  7432  fnn0nninf  10581  fsum2dlemstep  11687  fprod2dlemstep  11875  exmidunben  12739  prdsex  13043  isbasis3g  14460  tgcl  14478  tgss2  14493  blbas  14847  metrest  14920  dvmptfsum  15139  bdcuni  15745  bdcint  15746  bdcriota  15752  bdsep1  15754  bdsep2  15755  bdsepnft  15756  bdsepnf  15757  bdsepnfALT  15758  bdzfauscl  15759  bdbm1.3ii  15760  bj-axemptylem  15761  bj-axempty  15762  bj-axempty2  15763  bj-nalset  15764  bdinex1  15768  bj-zfpair2  15779  bj-axun2  15784  bj-uniex2  15785  bj-d0clsepcl  15794  bj-nn0suc0  15819  bj-nntrans  15820  bj-omex2  15846  strcollnft  15853  sscoll2  15857  nninfsellemcl  15881  nninfsellemsuc  15882  nninfsellemqall  15885  nninfomni  15889  exmidsbthrlem  15894