Theorem relssdv 5008

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

Step	Hyp	Ref	Expression
1		relssdv.2	. . 3 |- ( ph -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	alrimivv 1728	. 2 |- ( ph -> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
3		relssdv.1	. . 3 |- ( ph -> Rel A )
4		ssrel 5004	. . 3 |- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
5	3, 4	syl 16	. 2 |- ( ph -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
6	2, 5	mpbird 232	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1397   e. wcel 1826   C_ wss 3389   <.cop 3950   Rel wrel 4918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-opab 4426  df-xp 4919  df-rel 4920

This theorem is referenced by:  relssres  5223  poirr2  5304  sofld  5364  relssdmrn  5436  funcres2  15304  wunfunc  15305  fthres2  15338  pospo  15720  joindmss  15754  meetdmss  15768  clatl  15863  subrgdvds  17556  opsrtoslem2  18262  txcls  20190  txdis1cn  20221  txkgen  20238  qustgplem  20704  metustidOLD  21147  metustid  21148  metustexhalfOLD  21151  metustexhalf  21152  ovoliunlem1  21998  dvres2  22401  cvmlift2lem12  28948  dib2dim  37383  dih2dimbALTN  37385  dihmeetlem1N  37430  dihglblem5apreN  37431  dihmeetlem13N  37459  dihjatcclem4  37561