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

Theorem ssopab2i 4639
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 4637 . 2
2 ssopab2i.1 . . 3
32ax-gen 1570 . 2
41, 3mpg 1572 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1564  C_wss 3365  {copab 4375
This theorem is referenced by:  brab2a  4910  opabssxp  4933  funopab4  5473  ssoprab2i  6191  cardf2  7999  dfac3  8173  axdc2lem  8499  fpwwe2lem1  8677  canthwe  8697  fullfunc  14657  fthfunc  14658  isfull  14661  isfth  14665  ipoval  15165  ipolerval  15167  eqgfval  15559  2ndcctbss  18533  nvss  23093  ajfval  23331  cvmlift2lem12  26349  relopabVD  30483  dicval  33524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-in 3372  df-ss 3379  df-opab 4377
  Copyright terms: Public domain W3C validator