Theorem wel 2137

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

Syntax hints:   ∈ wcel 2136

This theorem is referenced by:  elequ1  2140  elequ2  2141  cleljust  2142  elsb1  2143  elsb2  2144  dveel1  2145  dveel2  2146  axext3  2148  axext4  2149  bm1.1  2150  ru  2950  nfuni  3795  nfunid  3796  unieq  3798  inteq  3827  nfint  3834  uniiun  3919  intiin  3920  trint  4095  axsep2  4101  bm1.3ii  4103  zfnuleu  4106  0ex  4109  nalset  4112  vnex  4113  repizf2  4141  axpweq  4150  zfpow  4154  axpow2  4155  axpow3  4156  el  4157  vpwex  4158  dtruarb  4170  exmidn0m  4180  exmidsssn  4181  fr0  4329  wetrep  4338  zfun  4412  axun2  4413  uniuni  4429  regexmid  4512  zfregfr  4551  ordwe  4553  wessep  4555  nnregexmid  4598  rele  4734  funimaexglem  5271  acexmidlem2  5839  acexmid  5841  dfsmo2  6255  smores2  6262  tfrcllemsucaccv  6322  findcard2d  6857  exmidfodomr  7160  acfun  7163  exmidontriimlem3  7179  exmidontriimlem4  7180  exmidontriim  7181  onntri13  7194  exmidontri  7195  onntri51  7196  onntri3or  7201  ccfunen  7205  cc1  7206  ltsopi  7261  fnn0nninf  10372  fsum2dlemstep  11375  fprod2dlemstep  11563  exmidunben  12359  isbasis3g  12694  tgcl  12714  tgss2  12729  blbas  13083  metrest  13156  bdcuni  13768  bdcint  13769  bdcriota  13775  bdsep1  13777  bdsep2  13778  bdsepnft  13779  bdsepnf  13780  bdsepnfALT  13781  bdzfauscl  13782  bdbm1.3ii  13783  bj-axemptylem  13784  bj-axempty  13785  bj-axempty2  13786  bj-nalset  13787  bdinex1  13791  bj-zfpair2  13802  bj-axun2  13807  bj-uniex2  13808  bj-d0clsepcl  13817  bj-nn0suc0  13842  bj-nntrans  13843  bj-omex2  13869  strcollnft  13876  sscoll2  13880  nninfsellemcl  13901  nninfsellemsuc  13902  nninfsellemqall  13905  nninfomni  13909  exmidsbthrlem  13911