Theorem ssopab2i 5551

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

Syntax hints:   → wi 4  ∀wal 1540   ⊆ wss 3949  {copab 5211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212

This theorem is referenced by:  elopabran  5563  elopaelxp  5766  opabssxp  5769  relopabiv  5821  funopab4  6586  ssoprab2i  7519  cnvoprab  8046  cardf2  9938  dfac3  10116  axdc2lem  10443  fpwwe2lem1  10626  canthwe  10646  trclublem  14942  fullfunc  17857  fthfunc  17858  isfull  17861  isfth  17865  ipoval  18483  ipolerval  18485  eqgfval  19056  2ndcctbss  22959  iscgrg  27763  ishpg  28010  nvss  29846  ajfval  30062  afsval  33683  cvmlift2lem12  34305  satf0suclem  34366  fmlasuc0  34375  bj-opabssvv  36031  bj-imdirval2lem  36063  bj-xpcossxp  36070  dicval  40047  areaquad  41965  relopabVD  43662