Theorem sseq2i 3951

Description: An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
sseq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
sseq2i	⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

Proof of Theorem sseq2i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		sseq2 3948	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sseqtri  3958  sseqtrdi  3972  abss  3995  ssrab  4007  ssindif0  4398  difcom  4420  ssunsn2  4761  ssunpr  4766  sspr  4767  sstp  4768  ssintrab  4903  iunpwss  5037  propssopi  5423  dffun2OLD  6448  ssimaex  6862  elpwun  7628  ssfi  8965  frfi  9068  alephislim  9848  cardaleph  9854  fin1a2lem12  10176  zornn0g  10270  ssxr  11053  nnwo  12662  isstruct  16862  issubm  18451  grpissubg  18784  islinds  21025  basdif0  22112  tgdif0  22151  cmpsublem  22559  cmpsub  22560  hauscmplem  22566  2ndcctbss  22615  fbncp  22999  cnextfval  23222  eltsms  23293  reconn  24000  cmssmscld  24523  axcontlem3  27343  axcontlem4  27344  umgredg  27517  nbuhgr  27719  uhgrvd00  27910  vtxdginducedm1  27919  chsscon1i  29833  hatomistici  30733  chirredlem4  30764  atabs2i  30773  mdsymlem1  30774  mdsymlem3  30776  mdsymlem6  30779  mdsymlem8  30781  dmdbr5ati  30793  iundifdif  30911  nocvxminlem  33981  nocvxmin  33982  poimir  35819  ismblfin  35827  cossssid2  36593  ntrk0kbimka  41656  ntrclsk3  41687  ntrneicls11  41707  abssf  42669  ssrabf  42671  stoweidlem57  43605  ovnsubadd  44117  ovnovollem3  44203  issubmgm  45354  linccl  45766  lincdifsn  45776