Theorem ssopab2i 4963

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

Syntax hints:   → wi 4  ∀wal 1478   ⊆ wss 3555  {copab 4672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-in 3562  df-ss 3569  df-opab 4674

This theorem is referenced by:  elopabran  4974  brab2a  5129  opabssxp  5154  funopab4  5883  ssoprab2i  6702  cardf2  8713  dfac3  8888  axdc2lem  9214  fpwwe2lem1  9397  canthwe  9417  trclublem  13668  fullfunc  16487  fthfunc  16488  isfull  16491  isfth  16495  ipoval  17075  ipolerval  17077  eqgfval  17563  2ndcctbss  21168  iscgrg  25307  ishpg  25551  pthsfval  26486  spthsfval  26487  crcts  26552  cycls  26553  eupths  26926  nvss  27294  ajfval  27510  afsval  30453  cvmlift2lem12  31001  dicval  35942  areaquad  37280  relopabVD  38617