Theorem relssdv 5773

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 1957	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		relssdv.1	. . 3 ⊢ (𝜑 → Rel 𝐴)
4		ssrel 5768	. . 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 1567   ∈ wcel 2142   ⊆ wss 3904  ⟨cop 4594  Rel wrel 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-opab 5173  df-xp 5666  df-rel 5667

This theorem is used by:  relssres  6020  poirr2  6123  sofld  6184  relssdmrn  6270  funcres2  17961  wunfunc  17964  fthres2  17997  pospo  18405  joindmss  18439  meetdmss  18453  clatl  18570  subrgdvds  20696  opsrtoslem2  22218  txcls  23772  txdis1cn  23803  txkgen  23820  qustgplem  24289  metustid  24722  metustexhalf  24724  ovoliunlem1  25672  dvres2  26082  cvmlift2lem12  35814  dib2dim  42045  dih2dimbALTN  42047  dihmeetlem1N  42092  dihglblem5apreN  42093  dihmeetlem13N  42121  dihjatcclem4  42223