Theorem ssopab2i 5412

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

Syntax hints:   → wi 4  ∀wal 1537   ⊆ wss 3861  {copab 5099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3868  df-ss 3878  df-opab 5100

This theorem is referenced by:  elopabran  5423  opabssxp  5618  relopabiv  5668  funopab4  6378  ssoprab2i  7264  cnvoprab  7769  cardf2  9419  dfac3  9595  axdc2lem  9922  fpwwe2lem1  10105  canthwe  10125  trclublem  14416  fullfunc  17250  fthfunc  17251  isfull  17254  isfth  17258  ipoval  17845  ipolerval  17847  eqgfval  18410  2ndcctbss  22170  iscgrg  26420  ishpg  26667  pthsfval  27624  spthsfval  27625  crcts  27691  cycls  27692  eupths  28099  nvss  28490  ajfval  28706  afsval  32184  cvmlift2lem12  32806  satf0suclem  32867  fmlasuc0  32876  bj-opabssvv  34881  bj-imdirval2lem  34913  bj-xpcossxp  34920  dicval  38788  areaquad  40585  relopabVD  42026