Theorem ssopab2i 5550

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3948  {copab 5210

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-opab 5211

This theorem is referenced by:  elopabran  5562  elopaelxp  5765  opabssxp  5768  relopabiv  5820  funopab4  6585  ssoprab2i  7522  cnvoprab  8050  mptmpoopabbrd  8071  cardf2  9944  dfac3  10122  axdc2lem  10449  fpwwe2lem1  10632  canthwe  10652  trclublem  14949  fullfunc  17866  fthfunc  17867  isfull  17870  isfth  17874  ipoval  18493  ipolerval  18495  eqgfval  19099  2ndcctbss  23279  iscgrg  28197  ishpg  28444  nvss  30280  ajfval  30496  afsval  34148  cvmlift2lem12  34770  satf0suclem  34831  fmlasuc0  34840  bj-opabssvv  36497  bj-imdirval2lem  36529  bj-xpcossxp  36536  dicval  40513  areaquad  42430  relopabVD  44127