Theorem wel 2142

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

Syntax hints:   ∈ wcel 2141

This theorem is referenced by:  elequ1  2145  elequ2  2146  cleljust  2147  elsb1  2148  elsb2  2149  dveel1  2150  dveel2  2151  axext3  2153  axext4  2154  bm1.1  2155  ru  2954  nfuni  3802  nfunid  3803  unieq  3805  inteq  3834  nfint  3841  uniiun  3926  intiin  3927  trint  4102  axsep2  4108  bm1.3ii  4110  zfnuleu  4113  0ex  4116  nalset  4119  vnex  4120  repizf2  4148  axpweq  4157  zfpow  4161  axpow2  4162  axpow3  4163  el  4164  vpwex  4165  dtruarb  4177  exmidn0m  4187  exmidsssn  4188  fr0  4336  wetrep  4345  zfun  4419  axun2  4420  uniuni  4436  regexmid  4519  zfregfr  4558  ordwe  4560  wessep  4562  nnregexmid  4605  rele  4741  funimaexglem  5281  acexmidlem2  5850  acexmid  5852  dfsmo2  6266  smores2  6273  tfrcllemsucaccv  6333  findcard2d  6869  exmidfodomr  7181  acfun  7184  exmidontriimlem3  7200  exmidontriimlem4  7201  exmidontriim  7202  onntri13  7215  exmidontri  7216  onntri51  7217  onntri3or  7222  ccfunen  7226  cc1  7227  ltsopi  7282  fnn0nninf  10393  fsum2dlemstep  11397  fprod2dlemstep  11585  exmidunben  12381  isbasis3g  12838  tgcl  12858  tgss2  12873  blbas  13227  metrest  13300  bdcuni  13911  bdcint  13912  bdcriota  13918  bdsep1  13920  bdsep2  13921  bdsepnft  13922  bdsepnf  13923  bdsepnfALT  13924  bdzfauscl  13925  bdbm1.3ii  13926  bj-axemptylem  13927  bj-axempty  13928  bj-axempty2  13929  bj-nalset  13930  bdinex1  13934  bj-zfpair2  13945  bj-axun2  13950  bj-uniex2  13951  bj-d0clsepcl  13960  bj-nn0suc0  13985  bj-nntrans  13986  bj-omex2  14012  strcollnft  14019  sscoll2  14023  nninfsellemcl  14044  nninfsellemsuc  14045  nninfsellemqall  14048  nninfomni  14052  exmidsbthrlem  14054