Theorem ssopab2i 5535

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

Syntax hints:   → wi 4  ∀wal 1568   ⊆ wss 3905  {copab 5173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ss 3922  df-opab 5174

This theorem is referenced by:  elopabran  5546  elopaelxp  5751  opabssxp  5753  relopabiv  5807  funopab4  6573  ssoprab2i  7521  cnvoprab  8053  mptmpoopabbrd  8074  enssdom  8969  cardf2  9925  dfac3  10101  axdc2lem  10427  fpwwe2lem1  10611  canthwe  10631  trclublem  15028  fullfunc  17960  fthfunc  17961  isfull  17964  isfth  17968  ipoval  18581  ipolerval  18583  eqgfval  19239  2ndcctbss  23612  iscgrg  28781  ishpg  29041  nvss  30945  ajfval  31161  afsval  35061  cvmlift2lem12  35806  satf0suclem  35867  fmlasuc0  35876  bj-opabssvv  37794  bj-imdirval2lem  37826  bj-xpcossxp  37833  dicval  41950  areaquad  43943  relopabVD  45609