Theorem relssdv 5043

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 1687	. 2 |- ( ph -> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
3		relssdv.1	. . 3 |- ( ph -> Rel A )
4		ssrel 5039	. . 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 1368   e. wcel 1758   C_ wss 3439   <.cop 3994   Rel wrel 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-opab 4462  df-xp 4957  df-rel 4958

This theorem is referenced by:  relssres  5258  poirr2  5333  sofld  5397  relssdmrn  5469  funcres2  14931  wunfunc  14932  fthres2  14965  pospo  15266  joindmss  15300  meetdmss  15314  clatl  15409  subrgdvds  17012  opsrtoslem2  17700  txcls  19319  txdis1cn  19350  txkgen  19367  divstgplem  19833  metustidOLD  20276  metustid  20277  metustexhalfOLD  20280  metustexhalf  20281  ovoliunlem1  21127  dvres2  21530  cvmlift2lem12  27370  dib2dim  35251  dih2dimbALTN  35253  dihmeetlem1N  35298  dihglblem5apreN  35299  dihmeetlem13N  35327  dihjatcclem4  35429