Theorem wel 2210

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

This proof depends on syntax axioms:   ∈ wcel 2209

This theorem is used by:  elequ1  2213  elequ2  2214  cleljust  2215  elsb1  2216  elsb2  2217  dveel1  2218  dveel2  2219  axext3  2221  axext4  2222  bm1.1  2223  ru  3050  nfuni  3941  nfunid  3942  unieq  3944  inteq  3973  nfint  3980  uniiun  4066  intiin  4067  trint  4244  axsepg  4250  sepg  4251  sepgi  4252  bm1.3ii  4254  zfnuleu  4257  0ex  4260  nalset  4263  vnex  4264  repizf2  4299  axpweq  4308  zfpow  4312  axpow2  4313  axpow3  4314  el  4315  vpwex  4316  dtruarb  4328  exmidn0m  4338  exmidsssn  4339  fr0  4496  wetrep  4505  zfun  4579  axun2  4580  uniex2  4581  uniuni  4597  regexmid  4682  zfregfr  4721  ordwe  4723  wessep  4725  nnregexmid  4768  rele  4910  funimaexglem  5464  acexmidlem2  6082  acexmid  6084  dfsmo2  6558  smores2  6565  tfrcllemsucaccv  6625  pw2f1odclem  7134  findcard2d  7195  sspw1or2  7544  exmidfodomr  7556  acfun  7563  exmidontriimlem3  7579  exmidontriimlem4  7580  exmidontriim  7581  onntri13  7597  exmidontri  7598  onntri51  7599  onntri3or  7604  exmidmotap  7627  ccfunen  7630  cc1  7631  ltsopi  7687  fnn0nninf  10875  hashfibclem  11282  fsum2dlemstep  12201  fprod2dlemstep  12389  exmidunben  13317  prdsex  14172  isbasis3g  15147  tgcl  15165  tgss2  15180  blbas  15534  metrest  15607  dvmptfsum  15826  uhgrfm  16314  ushgrfm  16315  uhgrss  16316  uhgreq12g  16317  uhgrfun  16318  ushgruhgr  16321  isuhgropm  16322  uhgr0e  16323  uhgr0vb  16325  uhgr0  16326  uhgrun  16327  bdcuni  16902  bdcint  16903  bdcriota  16909  bdsep1  16911  bdsep2  16912  bdsepnft  16913  bdsepnf  16914  bdsepnfALT  16915  bdsepg  16916  bdbm1.3ii  16917  bj-axemptylem  16918  bj-axempty  16919  bj-axempty2  16920  bj-nalset  16921  bdinex1  16925  bj-zfpair2  16936  bj-axun2  16941  bj-uniex2  16942  bj-d0clsepcl  16951  bj-nn0suc0  16976  bj-nntrans  16977  bj-omex2  17003  strcollnft  17010  sscoll2  17014  nninfsellemcl  17054  nninfsellemsuc  17055  nninfsellemqall  17058  nninfomni  17062  exmidsbthrlem  17067