Theorem ssopab2i 5493

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3903  {copab 5154

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ss 3920  df-opab 5155

This theorem is referenced by:  elopabran  5504  elopaelxp  5709  opabssxp  5711  relopabiv  5763  funopab4  6519  ssoprab2i  7460  cnvoprab  7995  mptmpoopabbrd  8015  cardf2  9839  dfac3  10015  axdc2lem  10342  fpwwe2lem1  10525  canthwe  10545  trclublem  14902  fullfunc  17815  fthfunc  17816  isfull  17819  isfth  17823  ipoval  18436  ipolerval  18438  eqgfval  19055  2ndcctbss  23340  iscgrg  28457  ishpg  28704  nvss  30537  ajfval  30753  afsval  34639  cvmlift2lem12  35287  satf0suclem  35348  fmlasuc0  35357  bj-opabssvv  37124  bj-imdirval2lem  37156  bj-xpcossxp  37163  dicval  41155  areaquad  43189  relopabVD  44874