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 1827	. 2 ⊢ ∀𝑦(𝜑 → 𝜓)
4	1, 3	mpg 1829	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ⊆ wss 3896  {copab 5166

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ss 3897  df-opab 5167

This theorem is used by:  elopabran  5536  elopaelxp  5742  opabssxp  5744  relopabiv  5799  funopab4  6582  ssoprab2i  7535  cnvoprab  8076  mptmpoopabbrd  8099  enssdom  9011  cardf2  10031  dfac3  10207  axdc2lem  10533  fpwwe2lem1  10723  canthwe  10743  trclublem  15157  fullfunc  18092  fthfunc  18093  isfull  18096  isfth  18100  ipoval  18713  ipolerval  18715  eqgfval  19397  2ndcctbss  23783  iscgrg  28984  ishpg  29246  nvss  31204  ajfval  31420  afsval  35353  cvmlift2lem12  36197  satf0suclem  36258  fmlasuc0  36267  bj-opabssvv  38208  bj-imdirval2lem  38240  bj-xpcossxp  38247  dicval  42370  areaquad  44355  relopabVD  46019