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

Theorem relssdv 4946
Description: Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)
Hypotheses
Ref Expression
relssdv.1  |-  ( ph  ->  Rel  A )
relssdv.2  |-  ( ph  ->  ( <. x ,  y
>.  e.  A  ->  <. x ,  y >.  e.  B
) )
Assertion
Ref Expression
relssdv  |-  ( ph  ->  A  C_  B )
Distinct variable groups:    x, y, A    x, B, y    ph, x, y

Proof of Theorem relssdv
StepHypRef Expression
1 relssdv.2 . . 3  |-  ( ph  ->  ( <. x ,  y
>.  e.  A  ->  <. x ,  y >.  e.  B
) )
21alrimivv 1768 . 2  |-  ( ph  ->  A. x A. y
( <. x ,  y
>.  e.  A  ->  <. x ,  y >.  e.  B
) )
3 relssdv.1 . . 3  |-  ( ph  ->  Rel  A )
4 ssrel 4942 . . 3  |-  ( Rel 
A  ->  ( A  C_  B  <->  A. x A. y
( <. x ,  y
>.  e.  A  ->  <. x ,  y >.  e.  B
) ) )
53, 4syl 17 . 2  |-  ( ph  ->  ( A  C_  B  <->  A. x A. y (
<. x ,  y >.  e.  A  ->  <. x ,  y >.  e.  B
) ) )
62, 5mpbird 235 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435    e. wcel 1872    C_ wss 3436   <.cop 4004   Rel wrel 4858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-opab 4483  df-xp 4859  df-rel 4860
This theorem is referenced by:  relssres  5161  poirr2  5243  sofld  5303  relssdmrn  5375  funcres2  15802  wunfunc  15803  fthres2  15836  pospo  16218  joindmss  16252  meetdmss  16266  clatl  16361  subrgdvds  18021  opsrtoslem2  18707  txcls  20617  txdis1cn  20648  txkgen  20665  qustgplem  21133  metustid  21567  metustexhalf  21569  ovoliunlem1  22453  dvres2  22865  cvmlift2lem12  30045  dib2dim  34780  dih2dimbALTN  34782  dihmeetlem1N  34827  dihglblem5apreN  34828  dihmeetlem13N  34856  dihjatcclem4  34958
  Copyright terms: Public domain W3C validator