MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  enqex Unicode version

Theorem enqex 8693
Description: The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
Assertion
Ref Expression
enqex  |-  ~Q  e.  _V

Proof of Theorem enqex
Dummy variables  x  y  z  w  v  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 niex 8652 . . . 4  |-  N.  e.  _V
21, 1xpex 4904 . . 3  |-  ( N. 
X.  N. )  e.  _V
32, 2xpex 4904 . 2  |-  ( ( N.  X.  N. )  X.  ( N.  X.  N. ) )  e.  _V
4 df-enq 8682 . . 3  |-  ~Q  =  { <. x ,  y
>.  |  ( (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u
)  =  ( w  .N  v ) ) ) }
5 opabssxp 4865 . . 3  |-  { <. x ,  y >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u
)  =  ( w  .N  v ) ) ) }  C_  (
( N.  X.  N. )  X.  ( N.  X.  N. ) )
64, 5eqsstri 3294 . 2  |-  ~Q  C_  (
( N.  X.  N. )  X.  ( N.  X.  N. ) )
73, 6ssexi 4261 1  |-  ~Q  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1546    = wceq 1647    e. wcel 1715   _Vcvv 2873   <.cop 3732   {copab 4178    X. cxp 4790  (class class class)co 5981   N.cnpi 8613    .N cmi 8615    ~Q ceq 8620
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615  ax-inf2 7489
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-sbc 3078  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-pss 3254  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-tp 3737  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-tr 4216  df-eprel 4408  df-po 4417  df-so 4418  df-fr 4455  df-we 4457  df-ord 4498  df-on 4499  df-lim 4500  df-suc 4501  df-om 4760  df-xp 4798  df-ni 8643  df-enq 8682
  Copyright terms: Public domain W3C validator