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

Theorem ssopab2i 4780
Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
Hypothesis
Ref Expression
ssopab2i.1
Assertion
Ref Expression
ssopab2i

Proof of Theorem ssopab2i
StepHypRef Expression
1 ssopab2 4778 . 2
2 ssopab2i.1 . . 3
32ax-gen 1618 . 2
41, 3mpg 1620 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  C_wss 3475  {copab 4509
This theorem is referenced by:  brab2a  5054  opabssxp  5079  funopab4  5628  ssoprab2i  6391  cardf2  8345  dfac3  8523  axdc2lem  8849  fpwwe2lem1  9030  canthwe  9050  fullfunc  15275  fthfunc  15276  isfull  15279  isfth  15283  ipoval  15784  ipolerval  15786  eqgfval  16249  2ndcctbss  19956  iscgrg  23904  ishpg  24128  nvss  25486  ajfval  25724  afsval  28551  cvmlift2lem12  28759  areaquad  31184  relopabVD  33701  dicval  36903  trclubg  37785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-opab 4511
  Copyright terms: Public domain W3C validator