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

Syntax hints:   → wi 4  ∀wal 1540   ⊆ wss 3889  {copab 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ss 3906  df-opab 5148

This theorem is referenced by:  elopabran  5516  elopaelxp  5721  opabssxp  5723  relopabiv  5776  funopab4  6535  ssoprab2i  7478  cnvoprab  8013  mptmpoopabbrd  8033  enssdom  8923  cardf2  9867  dfac3  10043  axdc2lem  10370  fpwwe2lem1  10554  canthwe  10574  trclublem  14957  fullfunc  17875  fthfunc  17876  isfull  17879  isfth  17883  ipoval  18496  ipolerval  18498  eqgfval  19151  2ndcctbss  23420  iscgrg  28580  ishpg  28827  nvss  30664  ajfval  30880  afsval  34815  cvmlift2lem12  35496  satf0suclem  35557  fmlasuc0  35566  bj-opabssvv  37464  bj-imdirval2lem  37496  bj-xpcossxp  37503  dicval  41622  areaquad  43644  relopabVD  45327