Theorem ssopab2i 5537

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ⊆ wss 3906  {copab 5175

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-ss 3923  df-opab 5176

This theorem is used by:  elopabran  5548  elopaelxp  5753  opabssxp  5755  relopabiv  5809  funopab4  6577  ssoprab2i  7530  cnvoprab  8063  mptmpoopabbrd  8084  enssdom  8979  cardf2  9945  dfac3  10121  axdc2lem  10447  fpwwe2lem1  10631  canthwe  10651  trclublem  15056  fullfunc  17987  fthfunc  17988  isfull  17991  isfth  17995  ipoval  18608  ipolerval  18610  eqgfval  19288  2ndcctbss  23663  iscgrg  28832  ishpg  29092  nvss  31016  ajfval  31232  afsval  35126  cvmlift2lem12  35843  satf0suclem  35904  fmlasuc0  35913  bj-opabssvv  37851  bj-imdirval2lem  37883  bj-xpcossxp  37890  dicval  42008  areaquad  44001  relopabVD  45667