Theorem ssopab2i 5560

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

Syntax hints:   → wi 4  ∀wal 1535   ⊆ wss 3963  {copab 5210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-ss 3980  df-opab 5211

This theorem is referenced by:  elopabran  5572  elopaelxp  5778  opabssxp  5781  relopabiv  5833  funopab4  6605  ssoprab2i  7544  cnvoprab  8084  mptmpoopabbrd  8104  cardf2  9981  dfac3  10159  axdc2lem  10486  fpwwe2lem1  10669  canthwe  10689  trclublem  15031  fullfunc  17960  fthfunc  17961  isfull  17964  isfth  17968  ipoval  18588  ipolerval  18590  eqgfval  19207  2ndcctbss  23479  iscgrg  28535  ishpg  28782  nvss  30622  ajfval  30838  afsval  34665  cvmlift2lem12  35299  satf0suclem  35360  fmlasuc0  35369  bj-opabssvv  37133  bj-imdirval2lem  37165  bj-xpcossxp  37172  dicval  41159  areaquad  43205  relopabVD  44899