Theorem ssopab2i 5456

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

Syntax hints:   → wi 4  ∀wal 1537   ⊆ wss 3883  {copab 5132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133

This theorem is referenced by:  elopabran  5467  opabssxp  5669  relopabiv  5719  funopab4  6455  ssoprab2i  7363  cnvoprab  7873  cardf2  9632  dfac3  9808  axdc2lem  10135  fpwwe2lem1  10318  canthwe  10338  trclublem  14634  fullfunc  17538  fthfunc  17539  isfull  17542  isfth  17546  ipoval  18163  ipolerval  18165  eqgfval  18719  2ndcctbss  22514  iscgrg  26777  ishpg  27024  pthsfval  27990  spthsfval  27991  crcts  28057  cycls  28058  eupths  28465  nvss  28856  ajfval  29072  afsval  32551  cvmlift2lem12  33176  satf0suclem  33237  fmlasuc0  33246  bj-opabssvv  35248  bj-imdirval2lem  35280  bj-xpcossxp  35287  dicval  39117  areaquad  40963  relopabVD  42410