Theorem ssopab2i 5488

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 5484	. 2 ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
2		ssopab2i.1	. . 3 ⊢ (𝜑 → 𝜓)
3	2	ax-gen 1796	. 2 ⊢ ∀𝑦(𝜑 → 𝜓)
4	1, 3	mpg 1798	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   → wi 4  ∀wal 1539   ⊆ wss 3897  {copab 5151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-ss 3914  df-opab 5152

This theorem is referenced by:  elopabran  5499  elopaelxp  5704  opabssxp  5706  relopabiv  5759  funopab4  6518  ssoprab2i  7457  cnvoprab  7992  mptmpoopabbrd  8012  cardf2  9836  dfac3  10012  axdc2lem  10339  fpwwe2lem1  10522  canthwe  10542  trclublem  14902  fullfunc  17815  fthfunc  17816  isfull  17819  isfth  17823  ipoval  18436  ipolerval  18438  eqgfval  19088  2ndcctbss  23370  iscgrg  28490  ishpg  28737  nvss  30573  ajfval  30789  afsval  34684  cvmlift2lem12  35358  satf0suclem  35419  fmlasuc0  35428  bj-opabssvv  37192  bj-imdirval2lem  37224  bj-xpcossxp  37231  dicval  41223  areaquad  43257  relopabVD  44941