Theorem ssopab2i 5506

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

Syntax hints:   → wi 4  ∀wal 1540   ⊆ wss 3903  {copab 5162

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 3920  df-opab 5163

This theorem is referenced by:  elopabran  5517  elopaelxp  5722  opabssxp  5724  relopabiv  5777  funopab4  6537  ssoprab2i  7479  cnvoprab  8014  mptmpoopabbrd  8034  enssdom  8925  cardf2  9867  dfac3  10043  axdc2lem  10370  fpwwe2lem1  10554  canthwe  10574  trclublem  14930  fullfunc  17844  fthfunc  17845  isfull  17848  isfth  17852  ipoval  18465  ipolerval  18467  eqgfval  19117  2ndcctbss  23411  iscgrg  28596  ishpg  28843  nvss  30681  ajfval  30897  afsval  34849  cvmlift2lem12  35530  satf0suclem  35591  fmlasuc0  35600  bj-opabssvv  37405  bj-imdirval2lem  37437  bj-xpcossxp  37444  dicval  41552  areaquad  43573  relopabVD  45256