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

Theorem ssopab2i 5141
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 5139 . 2 (∀𝑥𝑦(𝜑𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2 ssopab2i.1 . . 3 (𝜑𝜓)
32ax-gen 1859 . 2 𝑦(𝜑𝜓)
41, 3mpg 1861 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1618  wss 3703  {copab 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-in 3710  df-ss 3717  df-opab 4853
This theorem is referenced by:  elopabran  5152  opabssxp  5338  funopab4  6074  ssoprab2i  6902  cnvoprab  7385  cardf2  8930  dfac3  9105  axdc2lem  9433  fpwwe2lem1  9616  canthwe  9636  trclublem  13906  fullfunc  16738  fthfunc  16739  isfull  16742  isfth  16746  ipoval  17326  ipolerval  17328  eqgfval  17814  2ndcctbss  21431  iscgrg  25577  ishpg  25821  pthsfval  26798  spthsfval  26799  crcts  26865  cycls  26866  eupths  27323  nvss  27728  ajfval  27944  afsval  31029  cvmlift2lem12  31574  dicval  36936  areaquad  38273  relopabVD  39605
  Copyright terms: Public domain W3C validator