Theorem relssdv 5101

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 1696	. 2 |- ( ph -> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
3		relssdv.1	. . 3 |- ( ph -> Rel A )
4		ssrel 5097	. . 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 1377   e. wcel 1767   C_ wss 3481   <.cop 4039   Rel wrel 5010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-opab 4512  df-xp 5011  df-rel 5012

This theorem is referenced by:  relssres  5317  poirr2  5397  sofld  5461  relssdmrn  5534  funcres2  15142  wunfunc  15143  fthres2  15176  pospo  15477  joindmss  15511  meetdmss  15525  clatl  15620  subrgdvds  17314  opsrtoslem2  18019  txcls  19973  txdis1cn  20004  txkgen  20021  qustgplem  20487  metustidOLD  20930  metustid  20931  metustexhalfOLD  20934  metustexhalf  20935  ovoliunlem1  21781  dvres2  22184  cvmlift2lem12  28584  dib2dim  36441  dih2dimbALTN  36443  dihmeetlem1N  36488  dihglblem5apreN  36489  dihmeetlem13N  36517  dihjatcclem4  36619