Theorem relssdv 5661

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 1929	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		relssdv.1	. . 3 ⊢ (𝜑 → Rel 𝐴)
4		ssrel 5657	. . 3 ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
6	2, 5	mpbird 259	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   ∈ wcel 2114   ⊆ wss 3936  ⟨cop 4573  Rel wrel 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-opab 5129  df-xp 5561  df-rel 5562

This theorem is referenced by:  relssres  5893  poirr2  5984  sofld  6044  relssdmrn  6121  funcres2  17168  wunfunc  17169  fthres2  17202  pospo  17583  joindmss  17617  meetdmss  17631  clatl  17726  subrgdvds  19549  opsrtoslem2  20265  txcls  22212  txdis1cn  22243  txkgen  22260  qustgplem  22729  metustid  23164  metustexhalf  23166  ovoliunlem1  24103  dvres2  24510  cvmlift2lem12  32561  dib2dim  38394  dih2dimbALTN  38396  dihmeetlem1N  38441  dihglblem5apreN  38442  dihmeetlem13N  38470  dihjatcclem4  38572