Theorem ssopab2i 5505

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3911  {copab 5164

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ss 3928  df-opab 5165

This theorem is referenced by:  elopabran  5516  elopaelxp  5721  opabssxp  5723  relopabiv  5774  funopab4  6537  ssoprab2i  7480  cnvoprab  8018  mptmpoopabbrd  8038  cardf2  9872  dfac3  10050  axdc2lem  10377  fpwwe2lem1  10560  canthwe  10580  trclublem  14937  fullfunc  17846  fthfunc  17847  isfull  17850  isfth  17854  ipoval  18465  ipolerval  18467  eqgfval  19084  2ndcctbss  23318  iscgrg  28415  ishpg  28662  nvss  30495  ajfval  30711  afsval  34635  cvmlift2lem12  35274  satf0suclem  35335  fmlasuc0  35344  bj-opabssvv  37111  bj-imdirval2lem  37143  bj-xpcossxp  37150  dicval  41143  areaquad  43178  relopabVD  44863