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

Theorem ssopab2i 5428
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 5424 . 2 (∀𝑥𝑦(𝜑𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2 ssopab2i.1 . . 3 (𝜑𝜓)
32ax-gen 1787 . 2 𝑦(𝜑𝜓)
41, 3mpg 1789 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wss 3933  {copab 5119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-in 3940  df-ss 3949  df-opab 5120
This theorem is referenced by:  elopabran  5439  opabssxp  5636  relopabiv  5686  funopab4  6385  ssoprab2i  7252  cnvoprab  7747  cardf2  9360  dfac3  9535  axdc2lem  9858  fpwwe2lem1  10041  canthwe  10061  trclublem  14343  fullfunc  17164  fthfunc  17165  isfull  17168  isfth  17172  ipoval  17752  ipolerval  17754  eqgfval  18266  2ndcctbss  21991  iscgrg  26225  ishpg  26472  pthsfval  27429  spthsfval  27430  crcts  27496  cycls  27497  eupths  27906  nvss  28297  ajfval  28513  afsval  31841  cvmlift2lem12  32458  satf0suclem  32519  fmlasuc0  32528  bj-opabssvv  34334  bj-imdirval2  34365  dicval  38192  areaquad  39701  relopabVD  41112
  Copyright terms: Public domain W3C validator