Theorem ssopab2i 5001

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

Syntax hints:   → wi 4  ∀wal 1480   ⊆ wss 3572  {copab 4710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-in 3579  df-ss 3586  df-opab 4711

This theorem is referenced by:  elopabran  5012  opabssxp  5191  funopab4  5923  ssoprab2i  6746  cardf2  8766  dfac3  8941  axdc2lem  9267  fpwwe2lem1  9450  canthwe  9470  trclublem  13728  fullfunc  16560  fthfunc  16561  isfull  16564  isfth  16568  ipoval  17148  ipolerval  17150  eqgfval  17636  2ndcctbss  21252  iscgrg  25401  ishpg  25645  pthsfval  26611  spthsfval  26612  crcts  26677  cycls  26678  eupths  27053  nvss  27432  ajfval  27648  afsval  30734  cvmlift2lem12  31281  dicval  36291  areaquad  37628  relopabVD  38963