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

Theorem ssopab2i 5136
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 5134 . 2 (∀𝑥𝑦(𝜑𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2 ssopab2i.1 . . 3 (𝜑𝜓)
32ax-gen 1869 . 2 𝑦(𝜑𝜓)
41, 3mpg 1871 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1628  wss 3721  {copab 4844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-in 3728  df-ss 3735  df-opab 4845
This theorem is referenced by:  elopabran  5147  opabssxp  5333  funopab4  6068  ssoprab2i  6895  cnvoprab  7378  cardf2  8968  dfac3  9143  axdc2lem  9471  fpwwe2lem1  9654  canthwe  9674  trclublem  13943  fullfunc  16772  fthfunc  16773  isfull  16776  isfth  16780  ipoval  17361  ipolerval  17363  eqgfval  17849  2ndcctbss  21478  iscgrg  25627  ishpg  25871  pthsfval  26851  spthsfval  26852  crcts  26918  cycls  26919  eupths  27377  nvss  27782  ajfval  27998  afsval  31083  cvmlift2lem12  31628  dicval  36979  areaquad  38321  relopabVD  39653
  Copyright terms: Public domain W3C validator