Theorem sseq2i 3973

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 3970	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1540   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928

This theorem is referenced by:  sseqtrdi  3984  sseqtri  3992  abss  4023  ssrab  4032  ssindif0  4423  difcom  4448  ssunsn2  4787  ssunpr  4794  sspr  4795  sstp  4796  ssintrab  4931  iunpwss  5066  propssopi  5463  f1imadifssran  6586  ssimaex  6928  elpwun  7725  ssfi  9114  frfi  9208  alephislim  10012  cardaleph  10018  fin1a2lem12  10340  zornn0g  10434  ssxr  11219  nnwo  12848  isstruct  17098  issubmgm  18605  issubm  18706  grpissubg  19054  issubrng  20432  cntzsubrng  20452  islinds  21694  basdif0  22816  tgdif0  22855  cmpsublem  23262  cmpsub  23263  hauscmplem  23269  2ndcctbss  23318  fbncp  23702  cnextfval  23925  eltsms  23996  reconn  24693  cmssmscld  25226  nocvxminlem  27665  nocvxmin  27666  axcontlem3  28869  axcontlem4  28870  umgredg  29041  nbuhgr  29246  uhgrvd00  29438  vtxdginducedm1  29447  chsscon1i  31364  hatomistici  32264  chirredlem4  32295  atabs2i  32304  mdsymlem1  32305  mdsymlem3  32307  mdsymlem6  32310  mdsymlem8  32312  dmdbr5ati  32324  iundifdif  32464  poimir  37620  ismblfin  37628  cossssid2  38432  ntrk0kbimka  44001  ntrclsk3  44032  ntrneicls11  44052  wfaxrep  44957  wfaxsep  44958  abssf  45079  ssrabf  45081  stoweidlem57  46028  ovnsubadd  46543  ovnovollem3  46629  linccl  48376  lincdifsn  48386