Theorem relssdv 5761

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2145   ⊆ wss 3899  ⟨cop 4590  Rel wrel 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-opab 5168  df-xp 5654  df-rel 5655

This theorem is used by:  relssres  6010  poirr2  6113  sofld  6175  relssdmrn  6261  funcres2  18020  wunfunc  18023  fthres2  18056  pospo  18464  joindmss  18498  meetdmss  18512  clatl  18629  subrgdvds  20785  opsrtoslem2  22312  txcls  23870  txdis1cn  23901  txkgen  23918  qustgplem  24387  metustid  24820  metustexhalf  24822  ovoliunlem1  25770  dvres2  26179  cvmlift2lem12  35994  dib2dim  42214  dih2dimbALTN  42216  dihmeetlem1N  42261  dihglblem5apreN  42262  dihmeetlem13N  42290  dihjatcclem4  42392