Theorem relssdv 5736

Description: Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)

Hypotheses

Ref	Expression
relssdv.1	⊢ (𝜑 → Rel 𝐴)
relssdv.2	⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))

Assertion

Ref	Expression
relssdv	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜑,𝑥,𝑦

Proof of Theorem relssdv

Step	Hyp	Ref	Expression
1		relssdv.2	. . 3 ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	alrimivv 1930	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		relssdv.1	. . 3 ⊢ (𝜑 → Rel 𝐴)
4		ssrel 5731	. . 3 ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
6	2, 5	mpbird 257	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   ∈ wcel 2114   ⊆ wss 3900  ⟨cop 4585  Rel wrel 5628

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-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-opab 5160  df-xp 5629  df-rel 5630

This theorem is referenced by:  relssres  5980  poirr2  6080  sofld  6144  relssdmrn  6226  funcres2  17824  wunfunc  17827  fthres2  17860  pospo  18268  joindmss  18302  meetdmss  18316  clatl  18433  subrgdvds  20521  opsrtoslem2  22013  txcls  23550  txdis1cn  23581  txkgen  23598  qustgplem  24067  metustid  24500  metustexhalf  24502  ovoliunlem1  25461  dvres2  25871  cvmlift2lem12  35487  dib2dim  41538  dih2dimbALTN  41540  dihmeetlem1N  41585  dihglblem5apreN  41586  dihmeetlem13N  41614  dihjatcclem4  41716