Theorem ssopab2i 5505

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

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3911  {copab 5164

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ss 3928  df-opab 5165

This theorem is referenced by:  elopabran  5516  elopaelxp  5721  opabssxp  5723  relopabiv  5774  funopab4  6537  ssoprab2i  7480  cnvoprab  8018  mptmpoopabbrd  8038  cardf2  9872  dfac3  10050  axdc2lem  10377  fpwwe2lem1  10560  canthwe  10580  trclublem  14937  fullfunc  17850  fthfunc  17851  isfull  17854  isfth  17858  ipoval  18471  ipolerval  18473  eqgfval  19090  2ndcctbss  23375  iscgrg  28492  ishpg  28739  nvss  30572  ajfval  30788  afsval  34655  cvmlift2lem12  35294  satf0suclem  35355  fmlasuc0  35364  bj-opabssvv  37131  bj-imdirval2lem  37163  bj-xpcossxp  37170  dicval  41163  areaquad  43198  relopabVD  44883