Theorem ssopab2i 5496

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

Syntax hints:   → wi 4  ∀wal 1539   ⊆ wss 3899  {copab 5158

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-ss 3916  df-opab 5159

This theorem is referenced by:  elopabran  5507  elopaelxp  5712  opabssxp  5714  relopabiv  5767  funopab4  6527  ssoprab2i  7467  cnvoprab  8002  mptmpoopabbrd  8022  enssdom  8911  cardf2  9853  dfac3  10029  axdc2lem  10356  fpwwe2lem1  10540  canthwe  10560  trclublem  14916  fullfunc  17830  fthfunc  17831  isfull  17834  isfth  17838  ipoval  18451  ipolerval  18453  eqgfval  19103  2ndcctbss  23397  iscgrg  28533  ishpg  28780  nvss  30617  ajfval  30833  afsval  34777  cvmlift2lem12  35457  satf0suclem  35518  fmlasuc0  35527  bj-opabssvv  37294  bj-imdirval2lem  37326  bj-xpcossxp  37333  dicval  41375  areaquad  43400  relopabVD  45083