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  11716  fprod2dlemstep  11904  exmidunben  12768  prdsex  13072  isbasis3g  14489  tgcl  14507  tgss2  14522  blbas  14876  metrest  14949  dvmptfsum  15168  bdcuni  15774  bdcint  15775  bdcriota  15781  bdsep1  15783  bdsep2  15784  bdsepnft  15785  bdsepnf  15786  bdsepnfALT  15787  bdzfauscl  15788  bdbm1.3ii  15789  bj-axemptylem  15790  bj-axempty  15791  bj-axempty2  15792  bj-nalset  15793  bdinex1  15797  bj-zfpair2  15808  bj-axun2  15813  bj-uniex2  15814  bj-d0clsepcl  15823  bj-nn0suc0  15848  bj-nntrans  15849  bj-omex2  15875  strcollnft  15882  sscoll2  15886  nninfsellemcl  15910  nninfsellemsuc  15911  nninfsellemqall  15914  nninfomni  15918  exmidsbthrlem  15923