Theorem ssopab2i 5003

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

Syntax hints:   → wi 4  ∀wal 1481   ⊆ wss 3574  {copab 4712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-opab 4713

This theorem is referenced by:  elopabran  5014  opabssxp  5193  funopab4  5925  ssoprab2i  6749  cardf2  8769  dfac3  8944  axdc2lem  9270  fpwwe2lem1  9453  canthwe  9473  trclublem  13734  fullfunc  16566  fthfunc  16567  isfull  16570  isfth  16574  ipoval  17154  ipolerval  17156  eqgfval  17642  2ndcctbss  21258  iscgrg  25407  ishpg  25651  pthsfval  26617  spthsfval  26618  crcts  26683  cycls  26684  eupths  27060  nvss  27448  ajfval  27664  afsval  30749  cvmlift2lem12  31296  opabssi  34130  dicval  36465  areaquad  37802  relopabVD  39137