Theorem ssopab2i 5550

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

Syntax hints:   → wi 4  ∀wal 1539   ⊆ wss 3948  {copab 5210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-opab 5211

This theorem is referenced by:  elopabran  5562  elopaelxp  5765  opabssxp  5768  relopabiv  5820  funopab4  6585  ssoprab2i  7521  cnvoprab  8048  cardf2  9940  dfac3  10118  axdc2lem  10445  fpwwe2lem1  10628  canthwe  10648  trclublem  14944  fullfunc  17859  fthfunc  17860  isfull  17863  isfth  17867  ipoval  18485  ipolerval  18487  eqgfval  19058  2ndcctbss  22966  iscgrg  27801  ishpg  28048  nvss  29884  ajfval  30100  afsval  33752  cvmlift2lem12  34374  satf0suclem  34435  fmlasuc0  34444  bj-opabssvv  36117  bj-imdirval2lem  36149  bj-xpcossxp  36156  dicval  40133  areaquad  42047  relopabVD  43744