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

Theorem relssdv 5654
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 1920 . 2 (𝜑 → ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3 relssdv.1 . . 3 (𝜑 → Rel 𝐴)
4 ssrel 5650 . . 3 (Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
53, 4syl 17 . 2 (𝜑 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
62, 5mpbird 258 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526  wcel 2105  wss 3933  cop 4563  Rel wrel 5553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949  df-opab 5120  df-xp 5554  df-rel 5555
This theorem is referenced by:  relssres  5886  poirr2  5977  sofld  6037  relssdmrn  6114  funcres2  17156  wunfunc  17157  fthres2  17190  pospo  17571  joindmss  17605  meetdmss  17619  clatl  17714  subrgdvds  19478  opsrtoslem2  20193  txcls  22140  txdis1cn  22171  txkgen  22188  qustgplem  22656  metustid  23091  metustexhalf  23093  ovoliunlem1  24030  dvres2  24437  cvmlift2lem12  32458  dib2dim  38259  dih2dimbALTN  38261  dihmeetlem1N  38306  dihglblem5apreN  38307  dihmeetlem13N  38335  dihjatcclem4  38437
  Copyright terms: Public domain W3C validator