Theorem sseq2d 3186

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
sseq2d	|- ( ph -> ( C C_ A <-> C C_ B ) )

Proof of Theorem sseq2d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 |- ( ph -> A = B )
2		sseq2 3180	. 2 |- ( A = B -> ( C C_ A <-> C C_ B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C C_ A <-> C C_ B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   C_ wss 3130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  sseq12d  3187  sseqtrd  3194  exmidsssn  4203  exmidsssnc  4204  onsucsssucexmid  4527  sbcrel  4713  funimass2  5295  fnco  5325  fnssresb  5329  fnimaeq0  5338  foimacnv  5480  fvelimab  5573  ssimaexg  5579  fvmptss2  5592  rdgss  6384  tapeq2  7252  summodclem2  11390  summodc  11391  zsumdc  11392  fsum3cvg3  11404  prodmodclem2  11585  prodmodc  11586  zproddc  11587  ennnfoneleminc  12412  tgval  12711  releqgg  13080  eqgfval  13081  unitsubm  13288  subrgsubm  13355  issubrg3  13368  subrgpropd  13369  isbasisg  13547  tgss3  13581  restbasg  13671  tgrest  13672  restopn2  13686  cnpnei  13722  cnptopresti  13741  txbas  13761  elmopn  13949  neibl  13994  dvfgg  14160