Theorem sseq2i 3937

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseqtrdi  3948  sseqtri  3956  abss  3987  ssrab  3996  ssindif0  4416  difcom  4443  ssunsn2  4782  ssunpr  4788  sspr  4789  sstp  4790  ssintrab  4930  iunpwss  5066  propssopi  5479  imadifssrn  6201  ssimaex  6971  elpwun  7784  ssfi  9192  frfi  9280  alephislim  10166  cardaleph  10172  fin1a2lem12  10493  zornn0g  10587  ssxr  11383  nnwo  13044  isstruct  17336  issubmgm  18897  issubm  19004  grpissubg  19363  issubrng  20805  cntzsubrng  20825  rspvalint  21529  islinds  22121  basdif0  23277  tgdif0  23316  cmpsublem  23723  cmpsub  23724  hauscmplem  23730  2ndcctbss  23780  fbncp  24164  cnextfval  24387  eltsms  24458  reconn  25154  cmssmscld  25677  nobdaymin  28145  nocvxminlem  28146  axcontlem3  29550  axcontlem4  29551  umgredg  29722  nbuhgr  29930  uhgrvd00  30121  vtxdginducedm1  30130  chsscon1i  32070  hatomistici  32970  chirredlem4  33001  atabs2i  33010  mdsymlem1  33011  mdsymlem3  33013  mdsymlem6  33016  mdsymlem8  33018  dmdbr5ati  33030  iundifdif  33205  poimir  38665  ismblfin  38673  cossssid2  39584  ntrk0kbimka  45133  ntrclsk3  45164  ntrneicls11  45184  wfaxrep  46078  wfaxsep  46079  abssf  46221  ssrabf  46223  stoweidlem57  47161  ovnsubadd  47676  ovnovollem3  47762  grlimedgclnbgr  49187  linccl  49620  lincdifsn  49630