Theorem ssopab2i 5136

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

Syntax hints:   → wi 4  ∀wal 1628   ⊆ wss 3721  {copab 4844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-in 3728  df-ss 3735  df-opab 4845

This theorem is referenced by:  elopabran  5147  opabssxp  5333  funopab4  6068  ssoprab2i  6895  cnvoprab  7378  cardf2  8968  dfac3  9143  axdc2lem  9471  fpwwe2lem1  9654  canthwe  9674  trclublem  13943  fullfunc  16772  fthfunc  16773  isfull  16776  isfth  16780  ipoval  17361  ipolerval  17363  eqgfval  17849  2ndcctbss  21478  iscgrg  25627  ishpg  25871  pthsfval  26851  spthsfval  26852  crcts  26918  cycls  26919  eupths  27377  nvss  27782  ajfval  27998  afsval  31083  cvmlift2lem12  31628  dicval  36979  areaquad  38321  relopabVD  39653