Theorem ssopab2i 5555

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3951  {copab 5205

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ss 3968  df-opab 5206

This theorem is referenced by:  elopabran  5567  elopaelxp  5775  opabssxp  5778  relopabiv  5830  funopab4  6603  ssoprab2i  7544  cnvoprab  8085  mptmpoopabbrd  8105  cardf2  9983  dfac3  10161  axdc2lem  10488  fpwwe2lem1  10671  canthwe  10691  trclublem  15034  fullfunc  17953  fthfunc  17954  isfull  17957  isfth  17961  ipoval  18575  ipolerval  18577  eqgfval  19194  2ndcctbss  23463  iscgrg  28520  ishpg  28767  nvss  30612  ajfval  30828  afsval  34686  cvmlift2lem12  35319  satf0suclem  35380  fmlasuc0  35389  bj-opabssvv  37151  bj-imdirval2lem  37183  bj-xpcossxp  37190  dicval  41178  areaquad  43228  relopabVD  44921