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

Theorem ssopab2i 5508
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 5504 . 2 (∀𝑥𝑦(𝜑𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2 ssopab2i.1 . . 3 (𝜑𝜓)
32ax-gen 1798 . 2 𝑦(𝜑𝜓)
41, 3mpg 1800 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wss 3911  {copab 5168
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-opab 5169
This theorem is referenced by:  elopabran  5520  elopaelxp  5722  opabssxp  5725  relopabiv  5777  funopab4  6539  ssoprab2i  7468  cnvoprab  7993  cardf2  9880  dfac3  10058  axdc2lem  10385  fpwwe2lem1  10568  canthwe  10588  trclublem  14881  fullfunc  17794  fthfunc  17795  isfull  17798  isfth  17802  ipoval  18420  ipolerval  18422  eqgfval  18979  2ndcctbss  22809  iscgrg  27457  ishpg  27704  nvss  29538  ajfval  29754  afsval  33287  cvmlift2lem12  33911  satf0suclem  33972  fmlasuc0  33981  bj-opabssvv  35624  bj-imdirval2lem  35656  bj-xpcossxp  35663  dicval  39642  areaquad  41553  relopabVD  43190
  Copyright terms: Public domain W3C validator