Theorem ssopab2i 5538

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

Syntax hints:   → wi 4  ∀wal 1565   ⊆ wss 3913  {copab 5177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-ss 3930  df-opab 5178

This theorem is referenced by:  elopabran  5549  elopaelxp  5754  opabssxp  5756  relopabiv  5810  funopab4  6576  ssoprab2i  7524  cnvoprab  8059  mptmpoopabbrd  8080  enssdom  8975  cardf2  9931  dfac3  10107  axdc2lem  10434  fpwwe2lem1  10618  canthwe  10638  trclublem  15034  fullfunc  17967  fthfunc  17968  isfull  17971  isfth  17975  ipoval  18588  ipolerval  18590  eqgfval  19246  2ndcctbss  23583  iscgrg  28749  ishpg  29002  nvss  30888  ajfval  31104  afsval  35008  cvmlift2lem12  35741  satf0suclem  35802  fmlasuc0  35811  bj-opabssvv  37719  bj-imdirval2lem  37751  bj-xpcossxp  37758  dicval  41877  areaquad  43872  relopabVD  45538