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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  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  7518  cnvoprab  8045  cardf2  9937  dfac3  10115  axdc2lem  10442  fpwwe2lem1  10625  canthwe  10645  trclublem  14941  fullfunc  17856  fthfunc  17857  isfull  17860  isfth  17864  ipoval  18482  ipolerval  18484  eqgfval  19055  2ndcctbss  22958  iscgrg  27760  ishpg  28007  nvss  29841  ajfval  30057  afsval  33678  cvmlift2lem12  34300  satf0suclem  34361  fmlasuc0  34370  bj-opabssvv  36026  bj-imdirval2lem  36058  bj-xpcossxp  36065  dicval  40042  areaquad  41955  relopabVD  43652