Theorem ssopab2i 5521

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

Syntax hints:   → wi 4  ∀wal 1558   ⊆ wss 3904  {copab 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-ss 3921  df-opab 5163

This theorem is referenced by:  elopabran  5532  elopaelxp  5737  opabssxp  5739  relopabiv  5793  funopab4  6558  ssoprab2i  7507  cnvoprab  8041  mptmpoopabbrd  8062  enssdom  8957  cardf2  9901  dfac3  10077  axdc2lem  10405  fpwwe2lem1  10589  canthwe  10609  trclublem  15008  fullfunc  17941  fthfunc  17942  isfull  17945  isfth  17949  ipoval  18562  ipolerval  18564  eqgfval  19217  2ndcctbss  23515  iscgrg  28681  ishpg  28932  nvss  30796  ajfval  31012  afsval  34968  cvmlift2lem12  35664  satf0suclem  35725  fmlasuc0  35734  bj-opabssvv  37642  bj-imdirval2lem  37674  bj-xpcossxp  37681  dicval  41800  areaquad  43793  relopabVD  45476