Theorem ssopab2i 5532

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 5528	. 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 3900  {copab 5173

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ss 3901  df-opab 5174

This theorem is used by:  elopabran  5543  elopaelxp  5749  opabssxp  5751  relopabiv  5807  relopabi  5809  funopab4  6605  ssoprab2i  7562  cnvoprab  8106  mptmpoopabbrd  8129  enssdom  9041  cardf2  10061  dfac3  10239  axdc2lem  10565  fpwwe2lem1  10755  canthwe  10775  trclublem  15191  fullfunc  18133  fthfunc  18134  isfull  18137  isfth  18141  ipoval  18754  ipolerval  18756  eqgfval  19438  2ndcctbss  23829  iscgrg  29032  ishpg  29294  nvss  31252  ajfval  31468  afsval  35414  cvmlift2lem12  36287  satf0suclem  36348  fmlasuc0  36357  bj-opabssvv  38339  bj-imdirval2lem  38371  bj-xpcossxp  38378  dicval  42499  areaquad  44479  relopabVD  46143