Theorem ssopab2i 5513

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3917  {copab 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-ss 3934  df-opab 5173

This theorem is referenced by:  elopabran  5525  elopaelxp  5731  opabssxp  5734  relopabiv  5786  funopab4  6556  ssoprab2i  7503  cnvoprab  8042  mptmpoopabbrd  8062  cardf2  9903  dfac3  10081  axdc2lem  10408  fpwwe2lem1  10591  canthwe  10611  trclublem  14968  fullfunc  17877  fthfunc  17878  isfull  17881  isfth  17885  ipoval  18496  ipolerval  18498  eqgfval  19115  2ndcctbss  23349  iscgrg  28446  ishpg  28693  nvss  30529  ajfval  30745  afsval  34669  cvmlift2lem12  35308  satf0suclem  35369  fmlasuc0  35378  bj-opabssvv  37145  bj-imdirval2lem  37177  bj-xpcossxp  37184  dicval  41177  areaquad  43212  relopabVD  44897