Theorem ssopab2i 5510

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3914  {copab 5169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ss 3931  df-opab 5170

This theorem is referenced by:  elopabran  5522  elopaelxp  5728  opabssxp  5731  relopabiv  5783  funopab4  6553  ssoprab2i  7500  cnvoprab  8039  mptmpoopabbrd  8059  cardf2  9896  dfac3  10074  axdc2lem  10401  fpwwe2lem1  10584  canthwe  10604  trclublem  14961  fullfunc  17870  fthfunc  17871  isfull  17874  isfth  17878  ipoval  18489  ipolerval  18491  eqgfval  19108  2ndcctbss  23342  iscgrg  28439  ishpg  28686  nvss  30522  ajfval  30738  afsval  34662  cvmlift2lem12  35301  satf0suclem  35362  fmlasuc0  35371  bj-opabssvv  37138  bj-imdirval2lem  37170  bj-xpcossxp  37177  dicval  41170  areaquad  43205  relopabVD  44890