Theorem ssopab2i 5499

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

Syntax hints:   → wi 4  ∀wal 1540   ⊆ wss 3890  {copab 5148

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ss 3907  df-opab 5149

This theorem is referenced by:  elopabran  5510  elopaelxp  5715  opabssxp  5717  relopabiv  5770  funopab4  6530  ssoprab2i  7472  cnvoprab  8007  mptmpoopabbrd  8027  enssdom  8917  cardf2  9861  dfac3  10037  axdc2lem  10364  fpwwe2lem1  10548  canthwe  10568  trclublem  14951  fullfunc  17869  fthfunc  17870  isfull  17873  isfth  17877  ipoval  18490  ipolerval  18492  eqgfval  19145  2ndcctbss  23433  iscgrg  28597  ishpg  28844  nvss  30682  ajfval  30898  afsval  34834  cvmlift2lem12  35515  satf0suclem  35576  fmlasuc0  35585  bj-opabssvv  37483  bj-imdirval2lem  37515  bj-xpcossxp  37522  dicval  41639  areaquad  43665  relopabVD  45348