Theorem ssopab2i 5525

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ⊆ wss 3899  {copab 5167

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ss 3916  df-opab 5168

This theorem is used by:  elopabran  5536  elopaelxp  5741  opabssxp  5743  relopabiv  5798  funopab4  6577  ssoprab2i  7531  cnvoprab  8071  mptmpoopabbrd  8094  enssdom  9003  cardf2  10024  dfac3  10200  axdc2lem  10526  fpwwe2lem1  10716  canthwe  10736  trclublem  15148  fullfunc  18083  fthfunc  18084  isfull  18087  isfth  18091  ipoval  18704  ipolerval  18706  eqgfval  19388  2ndcctbss  23774  iscgrg  28975  ishpg  29237  nvss  31195  ajfval  31411  afsval  35303  cvmlift2lem12  36079  satf0suclem  36140  fmlasuc0  36149  bj-opabssvv  38071  bj-imdirval2lem  38103  bj-xpcossxp  38110  dicval  42233  areaquad  44217  relopabVD  45882