Theorem ssopab2i 5141

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

Syntax hints:   → wi 4  ∀wal 1618   ⊆ wss 3703  {copab 4852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-in 3710  df-ss 3717  df-opab 4853

This theorem is referenced by:  elopabran  5152  opabssxp  5338  funopab4  6074  ssoprab2i  6902  cnvoprab  7385  cardf2  8930  dfac3  9105  axdc2lem  9433  fpwwe2lem1  9616  canthwe  9636  trclublem  13906  fullfunc  16738  fthfunc  16739  isfull  16742  isfth  16746  ipoval  17326  ipolerval  17328  eqgfval  17814  2ndcctbss  21431  iscgrg  25577  ishpg  25821  pthsfval  26798  spthsfval  26799  crcts  26865  cycls  26866  eupths  27323  nvss  27728  ajfval  27944  afsval  31029  cvmlift2lem12  31574  dicval  36936  areaquad  38273  relopabVD  39605