Theorem ssopab2i 5498

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

Syntax hints:   → wi 4  ∀wal 1539   ⊆ wss 3901  {copab 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ss 3918  df-opab 5161

This theorem is referenced by:  elopabran  5509  elopaelxp  5714  opabssxp  5716  relopabiv  5769  funopab4  6529  ssoprab2i  7469  cnvoprab  8004  mptmpoopabbrd  8024  enssdom  8913  cardf2  9855  dfac3  10031  axdc2lem  10358  fpwwe2lem1  10542  canthwe  10562  trclublem  14918  fullfunc  17832  fthfunc  17833  isfull  17836  isfth  17840  ipoval  18453  ipolerval  18455  eqgfval  19105  2ndcctbss  23399  iscgrg  28584  ishpg  28831  nvss  30668  ajfval  30884  afsval  34828  cvmlift2lem12  35508  satf0suclem  35569  fmlasuc0  35578  bj-opabssvv  37355  bj-imdirval2lem  37387  bj-xpcossxp  37394  dicval  41436  areaquad  43458  relopabVD  45141