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

Theorem ssopab2i 4521
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 4519 . 2
2 ssopab2i.1 . . 3
32ax-gen 1556 . 2
41, 3mpg 1558 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1550  C_wss 3309  {copab 4300
This theorem is referenced by:  brab2a  4967  opabssxp  4990  funopab4  5535  ssoprab2i  6212  cardf2  7881  dfac3  8053  axdc2lem  8379  fpwwe2lem1  8557  canthwe  8577  fullfunc  14154  fthfunc  14155  isfull  14158  isfth  14162  ipoval  14631  ipolerval  14633  eqgfval  15039  2ndcctbss  17569  nvss  22123  ajfval  22361  cvmlift2lem12  25105  relopabVD  29254  dicval  32214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-in 3316  df-ss 3323  df-opab 4302
  Copyright terms: Public domain W3C validator