Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  relssdv Structured version   Visualization version   GIF version

Theorem relssdv 5649
 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
StepHypRef Expression
1 relssdv.2 . . 3 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
21alrimivv 1930 . 2 (𝜑 → ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3 relssdv.1 . . 3 (𝜑 → Rel 𝐴)
4 ssrel 5645 . . 3 (Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
53, 4syl 17 . 2 (𝜑 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
62, 5mpbird 260 1 (𝜑𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2115   ⊆ wss 3919  ⟨cop 4556  Rel wrel 5548 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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936  df-opab 5116  df-xp 5549  df-rel 5550 This theorem is referenced by:  relssres  5882  poirr2  5973  sofld  6033  relssdmrn  6110  funcres2  17170  wunfunc  17171  fthres2  17204  pospo  17585  joindmss  17619  meetdmss  17633  clatl  17728  subrgdvds  19551  opsrtoslem2  20733  txcls  22218  txdis1cn  22249  txkgen  22266  qustgplem  22735  metustid  23170  metustexhalf  23172  ovoliunlem1  24115  dvres2  24524  cvmlift2lem12  32646  dib2dim  38511  dih2dimbALTN  38513  dihmeetlem1N  38558  dihglblem5apreN  38559  dihmeetlem13N  38587  dihjatcclem4  38689
 Copyright terms: Public domain W3C validator