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 32117
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 2422 nor df-cleq 2434 (but of course using df-clab 2428 and df-clel 2437). Note that there is no dv condition on  x ,  y. Once extensionality is postulated, then isset 2974 will prove that "existing" (as a set) is equivalent to being a member of a class.

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

With ax-ext 2422, the present theorem is obvious from cbvexv 1977 and eqeq1 2447 (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 32116 . . . . 5  |-  x  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) }
32biantru 502 . . . 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 2437 . . 3  |-  ( A  e.  { z  |  ( z  =  z  ->  z  =  z ) }  <->  E. x
( x  =  A  /\  x  e.  {
z  |  ( z  =  z  ->  z  =  z ) } ) )
6 df-clel 2437 . . 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 32116 . . . . 5  |-  y  e. 
{ z  |  ( z  =  z  -> 
z  =  z ) }
98biantru 502 . . . 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 1364   E.wex 1591    e. wcel 1761   {cab 2427
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 1713  ax-7 1733  ax-12 1797
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-sb 1706  df-clab 2428  df-clel 2437
This theorem is referenced by:  bj-issetw  32118  bj-elisset  32120  bj-vtoclg1f1  32151
  Copyright terms: Public domain W3C validator