Theorem ssopab2i 5464

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

Step	Hyp	Ref	Expression
1		ssopab2 5460	. 2 ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2		ssopab2i.1	. . 3 ⊢ (𝜑 → 𝜓)
3	2	ax-gen 1798	. 2 ⊢ ∀𝑦(𝜑 → 𝜓)
4	1, 3	mpg 1800	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   → wi 4  ∀wal 1537   ⊆ wss 3888  {copab 5137

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-opab 5138

This theorem is referenced by:  elopabran  5476  elopaelxp  5677  opabssxp  5680  relopabiv  5732  funopab4  6478  ssoprab2i  7394  cnvoprab  7909  cardf2  9710  dfac3  9886  axdc2lem  10213  fpwwe2lem1  10396  canthwe  10416  trclublem  14715  fullfunc  17631  fthfunc  17632  isfull  17635  isfth  17639  ipoval  18257  ipolerval  18259  eqgfval  18813  2ndcctbss  22615  iscgrg  26882  ishpg  27129  nvss  28964  ajfval  29180  afsval  32660  cvmlift2lem12  33285  satf0suclem  33346  fmlasuc0  33355  bj-opabssvv  35330  bj-imdirval2lem  35362  bj-xpcossxp  35369  dicval  39197  areaquad  41054  relopabVD  42528