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

Theorem ssopab2i 5412
 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 5408 . 2 (∀𝑥𝑦(𝜑𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2 ssopab2i.1 . . 3 (𝜑𝜓)
32ax-gen 1798 . 2 𝑦(𝜑𝜓)
41, 3mpg 1800 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1537   ⊆ wss 3861  {copab 5099 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3868  df-ss 3878  df-opab 5100 This theorem is referenced by:  elopabran  5423  opabssxp  5618  relopabiv  5668  funopab4  6378  ssoprab2i  7264  cnvoprab  7769  cardf2  9419  dfac3  9595  axdc2lem  9922  fpwwe2lem1  10105  canthwe  10125  trclublem  14416  fullfunc  17250  fthfunc  17251  isfull  17254  isfth  17258  ipoval  17845  ipolerval  17847  eqgfval  18410  2ndcctbss  22170  iscgrg  26420  ishpg  26667  pthsfval  27624  spthsfval  27625  crcts  27691  cycls  27692  eupths  28099  nvss  28490  ajfval  28706  afsval  32184  cvmlift2lem12  32806  satf0suclem  32867  fmlasuc0  32876  bj-opabssvv  34881  bj-imdirval2lem  34913  bj-xpcossxp  34920  dicval  38788  areaquad  40585  relopabVD  42026
 Copyright terms: Public domain W3C validator