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 34146
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 2419 nor df-cleq 2433 (but of course using df-clab 2427 and df-clel 2436). Once extensionality is postulated, then isset 3097 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 1983. Actually, the proof depends only on ax-1--7 and sp 1843.

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 2419 (e.g. eqid 2441). In particular, one cannot even prove  |-  E. x x  =  A => 
|-  A  =  A.

With ax-ext 2419, the present theorem is obvious from cbvexv 2008 and eqeq1 2445 (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 34145 . . . . 5  |-  x  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) }
32biantru 505 . . . 4  |-  ( x  =  A  <->  ( x  =  A  /\  x  e.  { z  |  ( z  =  z  -> 
z  =  z ) } ) )
43exbii 1652 . . 3  |-  ( E. x  x  =  A  <->  E. x ( x  =  A  /\  x  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) } ) )
5 df-clel 2436 . . 3  |-  ( A  e.  { z  |  ( z  =  z  ->  z  =  z ) }  <->  E. x
( x  =  A  /\  x  e.  {
z  |  ( z  =  z  ->  z  =  z ) } ) )
6 df-clel 2436 . . 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 34145 . . . . 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 1652 . 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 1381   E.wex 1597    e. wcel 1802   {cab 2426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-sb 1725  df-clab 2427  df-clel 2436
This theorem is referenced by:  bj-issetwt  34147  bj-elisset  34150  bj-vtoclg1f1  34194
  Copyright terms: Public domain W3C validator