Theorem ssopab2i 5437

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

Syntax hints:   → wi 4  ∀wal 1535   ⊆ wss 3936  {copab 5128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-opab 5129

This theorem is referenced by:  elopabran  5448  opabssxp  5643  relopabiv  5693  funopab4  6392  ssoprab2i  7263  cnvoprab  7758  cardf2  9372  dfac3  9547  axdc2lem  9870  fpwwe2lem1  10053  canthwe  10073  trclublem  14355  fullfunc  17176  fthfunc  17177  isfull  17180  isfth  17184  ipoval  17764  ipolerval  17766  eqgfval  18328  2ndcctbss  22063  iscgrg  26298  ishpg  26545  pthsfval  27502  spthsfval  27503  crcts  27569  cycls  27570  eupths  27979  nvss  28370  ajfval  28586  afsval  31942  cvmlift2lem12  32561  satf0suclem  32622  fmlasuc0  32631  bj-opabssvv  34445  bj-imdirval2  34476  dicval  38327  areaquad  39843  relopabVD  41255