Theorem ssopab2i 5536

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

Syntax hints:   → wi 4  ∀wal 1565   ⊆ wss 3913  {copab 5177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-ss 3930  df-opab 5178

This theorem is referenced by:  elopabran  5547  elopaelxp  5752  opabssxp  5754  relopabiv  5808  funopab4  6574  ssoprab2i  7522  cnvoprab  8056  mptmpoopabbrd  8077  enssdom  8972  cardf2  9928  dfac3  10104  axdc2lem  10431  fpwwe2lem1  10615  canthwe  10635  trclublem  15031  fullfunc  17964  fthfunc  17965  isfull  17968  isfth  17972  ipoval  18585  ipolerval  18587  eqgfval  19243  2ndcctbss  23580  iscgrg  28746  ishpg  28999  nvss  30885  ajfval  31101  afsval  35005  cvmlift2lem12  35704  satf0suclem  35765  fmlasuc0  35774  bj-opabssvv  37681  bj-imdirval2lem  37713  bj-xpcossxp  37720  dicval  41839  areaquad  43834  relopabVD  45500