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

Theorem relssdv 5749
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 1932 . 2 (𝜑 → ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3 relssdv.1 . . 3 (𝜑 → Rel 𝐴)
4 ssrel 5743 . . 3 (Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
53, 4syl 17 . 2 (𝜑 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
62, 5mpbird 257 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  wcel 2107  wss 3915  cop 4597  Rel wrel 5643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-opab 5173  df-xp 5644  df-rel 5645
This theorem is referenced by:  relssres  5983  poirr2  6083  sofld  6144  relssdmrn  6225  relssdmrnOLD  6226  funcres2  17791  wunfunc  17792  wunfuncOLD  17793  fthres2  17826  pospo  18241  joindmss  18275  meetdmss  18289  clatl  18404  subrgdvds  20252  opsrtoslem2  21479  txcls  22971  txdis1cn  23002  txkgen  23019  qustgplem  23488  metustid  23926  metustexhalf  23928  ovoliunlem1  24882  dvres2  25292  cvmlift2lem12  33948  dib2dim  39735  dih2dimbALTN  39737  dihmeetlem1N  39782  dihglblem5apreN  39783  dihmeetlem13N  39811  dihjatcclem4  39913
  Copyright terms: Public domain W3C validator