Theorem wel 2168

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

Syntax hints:   ∈ wcel 2167

This theorem is referenced by:  elequ1  2171  elequ2  2172  cleljust  2173  elsb1  2174  elsb2  2175  dveel1  2176  dveel2  2177  axext3  2179  axext4  2180  bm1.1  2181  ru  2988  nfuni  3845  nfunid  3846  unieq  3848  inteq  3877  nfint  3884  uniiun  3970  intiin  3971  trint  4146  axsep2  4152  bm1.3ii  4154  zfnuleu  4157  0ex  4160  nalset  4163  vnex  4164  repizf2  4195  axpweq  4204  zfpow  4208  axpow2  4209  axpow3  4210  el  4211  vpwex  4212  dtruarb  4224  exmidn0m  4234  exmidsssn  4235  fr0  4386  wetrep  4395  zfun  4469  axun2  4470  uniuni  4486  regexmid  4571  zfregfr  4610  ordwe  4612  wessep  4614  nnregexmid  4657  rele  4796  funimaexglem  5341  acexmidlem2  5919  acexmid  5921  dfsmo2  6345  smores2  6352  tfrcllemsucaccv  6412  pw2f1odclem  6895  findcard2d  6952  exmidfodomr  7271  acfun  7274  exmidontriimlem3  7290  exmidontriimlem4  7291  exmidontriim  7292  onntri13  7305  exmidontri  7306  onntri51  7307  onntri3or  7312  exmidmotap  7328  ccfunen  7331  cc1  7332  ltsopi  7387  fnn0nninf  10530  fsum2dlemstep  11599  fprod2dlemstep  11787  exmidunben  12643  prdsex  12940  isbasis3g  14282  tgcl  14300  tgss2  14315  blbas  14669  metrest  14742  dvmptfsum  14961  bdcuni  15522  bdcint  15523  bdcriota  15529  bdsep1  15531  bdsep2  15532  bdsepnft  15533  bdsepnf  15534  bdsepnfALT  15535  bdzfauscl  15536  bdbm1.3ii  15537  bj-axemptylem  15538  bj-axempty  15539  bj-axempty2  15540  bj-nalset  15541  bdinex1  15545  bj-zfpair2  15556  bj-axun2  15561  bj-uniex2  15562  bj-d0clsepcl  15571  bj-nn0suc0  15596  bj-nntrans  15597  bj-omex2  15623  strcollnft  15630  sscoll2  15634  nninfsellemcl  15655  nninfsellemsuc  15656  nninfsellemqall  15659  nninfomni  15663  exmidsbthrlem  15666