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

Step	Hyp	Ref	Expression
1		relssdv.2	. . 3 |- ( ph -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2	1	alrimivv 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 ) ) )
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 235	1 |- ( ph -> A C_ B )

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