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

Theorem ssopab2i 4621
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 4619 . 2
2 ssopab2i.1 . . 3
32ax-gen 1562 . 2
41, 3mpg 1564 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1556  C_wss 3353  {copab 4359
This theorem is referenced by:  brab2a  4892  opabssxp  4915  funopab4  5452  ssoprab2i  6151  cardf2  7944  dfac3  8116  axdc2lem  8442  fpwwe2lem1  8620  canthwe  8640  fullfunc  14594  fthfunc  14595  isfull  14598  isfth  14602  ipoval  15102  ipolerval  15104  eqgfval  15491  2ndcctbss  18022  nvss  22581  ajfval  22819  cvmlift2lem12  25840  relopabVD  30206  dicval  33247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-in 3360  df-ss 3367  df-opab 4361
  Copyright terms: Public domain W3C validator