Theorem ssopab2i 5492

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

Syntax hints:   → wi 4  ∀wal 1545   ⊆ wss 3883  {copab 5134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-ss 3900  df-opab 5135

This theorem is referenced by:  elopabran  5503  elopaelxp  5708  opabssxp  5710  relopabiv  5763  funopab4  6522  ssoprab2i  7467  cnvoprab  8002  mptmpoopabbrd  8022  enssdom  8913  cardf2  9858  dfac3  10034  axdc2lem  10361  fpwwe2lem1  10545  canthwe  10565  trclublem  14948  fullfunc  17866  fthfunc  17867  isfull  17870  isfth  17874  ipoval  18487  ipolerval  18489  eqgfval  19142  2ndcctbss  23438  iscgrg  28598  ishpg  28845  nvss  30682  ajfval  30898  afsval  34855  cvmlift2lem12  35542  satf0suclem  35603  fmlasuc0  35612  bj-opabssvv  37510  bj-imdirval2lem  37542  bj-xpcossxp  37549  dicval  41668  areaquad  43661  relopabVD  45344