Theorem ssopab2i 5529

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 5525	. 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 3899  {copab 5167

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 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-ss 3916  df-opab 5168

This theorem is used by:  elopabran  5540  elopaelxp  5745  opabssxp  5747  relopabiv  5801  funopab4  6570  ssoprab2i  7524  cnvoprab  8057  mptmpoopabbrd  8080  enssdom  8982  cardf2  9948  dfac3  10124  axdc2lem  10450  fpwwe2lem1  10640  canthwe  10660  trclublem  15068  fullfunc  17997  fthfunc  17998  isfull  18001  isfth  18005  ipoval  18618  ipolerval  18620  eqgfval  19301  2ndcctbss  23681  iscgrg  28854  ishpg  29116  nvss  31074  ajfval  31290  afsval  35182  cvmlift2lem12  35893  satf0suclem  35954  fmlasuc0  35963  bj-opabssvv  37902  bj-imdirval2lem  37934  bj-xpcossxp  37941  dicval  42049  areaquad  44057  relopabVD  45723