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

Theorem ssopab2i 5001
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 4999 . 2 (∀𝑥𝑦(𝜑𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2 ssopab2i.1 . . 3 (𝜑𝜓)
32ax-gen 1721 . 2 𝑦(𝜑𝜓)
41, 3mpg 1723 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1480  wss 3572  {copab 4710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-in 3579  df-ss 3586  df-opab 4711
This theorem is referenced by:  elopabran  5012  opabssxp  5191  funopab4  5923  ssoprab2i  6746  cardf2  8766  dfac3  8941  axdc2lem  9267  fpwwe2lem1  9450  canthwe  9470  trclublem  13728  fullfunc  16560  fthfunc  16561  isfull  16564  isfth  16568  ipoval  17148  ipolerval  17150  eqgfval  17636  2ndcctbss  21252  iscgrg  25401  ishpg  25645  pthsfval  26611  spthsfval  26612  crcts  26677  cycls  26678  eupths  27053  nvss  27432  ajfval  27648  afsval  30734  cvmlift2lem12  31281  dicval  36291  areaquad  37628  relopabVD  38963
  Copyright terms: Public domain W3C validator