Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-denotes Structured version   Unicode version

Theorem bj-denotes 33390
Description: This would be the justification for the definition of the unary predicate "E!" by  |-  ( E!  A  <->  E. x x  =  A ) which could be interpreted as " A exists" or " A denotes". It is interesting that this justification can be proved without ax-ext 2438 nor df-cleq 2452 (but of course using df-clab 2446 and df-clel 2455). Once extensionality is postulated, then isset 3110 will prove that "existing" (as a set) is equivalent to being a member of a class.

Note that there is no dv condition on  x ,  y but the theorem does not depend on ax-13 1961. Actually, the proof depends only on ax-1--7 and sp 1803.

The symbol "E!" was chosen to be reminiscent of the analogous predicate in (inclusive or non-inclusive) free logic, which deals with the possibility of non-existent objects. This analogy should not be taken too far, since here there are no equality axioms for classes: they are derived from ax-ext 2438 (e.g. eqid 2460). In particular, one cannot even prove  |-  E. x x  =  A => 
|-  A  =  A.

With ax-ext 2438, the present theorem is obvious from cbvexv 1990 and eqeq1 2464 (in free logic, the same proof holds since one has equality axioms for terms). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)

Assertion
Ref Expression
bj-denotes  |-  ( E. x  x  =  A  <->  E. y  y  =  A )
Distinct variable groups:    x, A    y, A

Proof of Theorem bj-denotes
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . . 6  |-  ( z  =  z  ->  z  =  z )
21bj-vexwv 33389 . . . . 5  |-  x  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) }
32biantru 505 . . . 4  |-  ( x  =  A  <->  ( x  =  A  /\  x  e.  { z  |  ( z  =  z  -> 
z  =  z ) } ) )
43exbii 1639 . . 3  |-  ( E. x  x  =  A  <->  E. x ( x  =  A  /\  x  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) } ) )
5 df-clel 2455 . . 3  |-  ( A  e.  { z  |  ( z  =  z  ->  z  =  z ) }  <->  E. x
( x  =  A  /\  x  e.  {
z  |  ( z  =  z  ->  z  =  z ) } ) )
6 df-clel 2455 . . 3  |-  ( A  e.  { z  |  ( z  =  z  ->  z  =  z ) }  <->  E. y
( y  =  A  /\  y  e.  {
z  |  ( z  =  z  ->  z  =  z ) } ) )
74, 5, 63bitr2i 273 . 2  |-  ( E. x  x  =  A  <->  E. y ( y  =  A  /\  y  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) } ) )
81bj-vexwv 33389 . . . . 5  |-  y  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) }
98biantru 505 . . . 4  |-  ( y  =  A  <->  ( y  =  A  /\  y  e.  { z  |  ( z  =  z  -> 
z  =  z ) } ) )
109bicomi 202 . . 3  |-  ( ( y  =  A  /\  y  e.  { z  |  ( z  =  z  ->  z  =  z ) } )  <-> 
y  =  A )
1110exbii 1639 . 2  |-  ( E. y ( y  =  A  /\  y  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) } )  <->  E. y 
y  =  A )
127, 11bitri 249 1  |-  ( E. x  x  =  A  <->  E. y  y  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374   E.wex 1591    e. wcel 1762   {cab 2445
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-sb 1707  df-clab 2446  df-clel 2455
This theorem is referenced by:  bj-issetwt  33391  bj-elisset  33394  bj-vtoclg1f1  33438
  Copyright terms: Public domain W3C validator