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

Theorem ssopab2i 5555
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 5551 . 2 (∀𝑥𝑦(𝜑𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2 ssopab2i.1 . . 3 (𝜑𝜓)
32ax-gen 1795 . 2 𝑦(𝜑𝜓)
41, 3mpg 1797 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538  wss 3951  {copab 5205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ss 3968  df-opab 5206
This theorem is referenced by:  elopabran  5567  elopaelxp  5775  opabssxp  5778  relopabiv  5830  funopab4  6603  ssoprab2i  7544  cnvoprab  8085  mptmpoopabbrd  8105  cardf2  9983  dfac3  10161  axdc2lem  10488  fpwwe2lem1  10671  canthwe  10691  trclublem  15034  fullfunc  17953  fthfunc  17954  isfull  17957  isfth  17961  ipoval  18575  ipolerval  18577  eqgfval  19194  2ndcctbss  23463  iscgrg  28520  ishpg  28767  nvss  30612  ajfval  30828  afsval  34686  cvmlift2lem12  35319  satf0suclem  35380  fmlasuc0  35389  bj-opabssvv  37151  bj-imdirval2lem  37183  bj-xpcossxp  37190  dicval  41178  areaquad  43228  relopabVD  44921
  Copyright terms: Public domain W3C validator