Theorem ssopab2i 5569

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

Syntax hints:   → wi 4  ∀wal 1535   ⊆ wss 3976  {copab 5228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ss 3993  df-opab 5229

This theorem is referenced by:  elopabran  5581  elopaelxp  5789  opabssxp  5792  relopabiv  5844  funopab4  6615  ssoprab2i  7561  cnvoprab  8101  mptmpoopabbrd  8121  cardf2  10012  dfac3  10190  axdc2lem  10517  fpwwe2lem1  10700  canthwe  10720  trclublem  15044  fullfunc  17973  fthfunc  17974  isfull  17977  isfth  17981  ipoval  18600  ipolerval  18602  eqgfval  19216  2ndcctbss  23484  iscgrg  28538  ishpg  28785  nvss  30625  ajfval  30841  afsval  34648  cvmlift2lem12  35282  satf0suclem  35343  fmlasuc0  35352  bj-opabssvv  37116  bj-imdirval2lem  37148  bj-xpcossxp  37155  dicval  41133  areaquad  43177  relopabVD  44872