Theorem ssopab2i 5525

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3926  {copab 5181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-ss 3943  df-opab 5182

This theorem is referenced by:  elopabran  5537  elopaelxp  5744  opabssxp  5747  relopabiv  5799  funopab4  6573  ssoprab2i  7518  cnvoprab  8059  mptmpoopabbrd  8079  cardf2  9957  dfac3  10135  axdc2lem  10462  fpwwe2lem1  10645  canthwe  10665  trclublem  15014  fullfunc  17921  fthfunc  17922  isfull  17925  isfth  17929  ipoval  18540  ipolerval  18542  eqgfval  19159  2ndcctbss  23393  iscgrg  28491  ishpg  28738  nvss  30574  ajfval  30790  afsval  34703  cvmlift2lem12  35336  satf0suclem  35397  fmlasuc0  35406  bj-opabssvv  37168  bj-imdirval2lem  37200  bj-xpcossxp  37207  dicval  41195  areaquad  43240  relopabVD  44925