Theorem relssdv 4905

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 1778	. 2 |- ( ph -> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
3		relssdv.1	. . 3 |- ( ph -> Rel A )
4		ssrel 4901	. . 3 |- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
5	3, 4	syl 17	. 2 |- ( ph -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
6	2, 5	mpbird 240	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   <-> wb 189   A.wal 1446   e. wcel 1891   C_ wss 3372   <.cop 3942   Rel wrel 4817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pr 4612

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-opab 4434  df-xp 4818  df-rel 4819

This theorem is referenced by:  relssres  5120  poirr2  5202  sofld  5262  relssdmrn  5335  funcres2  15814  wunfunc  15815  fthres2  15848  pospo  16230  joindmss  16264  meetdmss  16278  clatl  16373  subrgdvds  18033  opsrtoslem2  18719  txcls  20630  txdis1cn  20661  txkgen  20678  qustgplem  21146  metustid  21580  metustexhalf  21582  ovoliunlem1  22466  dvres2  22879  cvmlift2lem12  30043  dib2dim  34813  dih2dimbALTN  34815  dihmeetlem1N  34860  dihglblem5apreN  34861  dihmeetlem13N  34889  dihjatcclem4  34991