Theorem sseq2 4009

Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)

Assertion

Ref	Expression
sseq2	⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 3990	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3990	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3998	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 476	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ⊆ wss 3949

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sseq12  4010  sseq2i  4012  sseq2d  4015  nssne1  4045  psseq2  4089  sseq0  4400  un00  4443  disjpss  4461  pweqALT  4618  ssintab  4970  ssintub  4971  intmin  4973  treq  5274  al0ssb  5309  sseliALT  5310  ssexg  5324  intabs  5343  iunopeqop  5522  onelssex  6413  ordunidif  6414  ordssun  6467  fununi  6624  feq3  6701  ssimaexg  6978  fnssintima  7359  iunpw  7758  tfindsg  7850  limomss  7860  findsg  7890  funcnvuni  7922  frxp  8112  frrlem1  8271  frrlem13  8283  wrecseq123OLD  8300  wfrlem1OLD  8308  wfrlem4OLD  8312  wfrlem15OLD  8323  onfununi  8341  oawordeu  8555  oawordexr  8556  nnawordex  8637  eldifsucnn  8663  coflton  8670  cofon1  8671  cofon2  8672  cofonr  8673  naddcllem  8675  naddunif  8692  ereq1  8710  xpider  8782  domeng  8958  sbthlem4  9086  sbthlem5  9087  domssex  9138  ssfi  9173  finsschain  9359  dffi2  9418  dffi3  9426  hartogslem1  9537  inf3lema  9619  cantnflem1  9684  dfttrcl2  9719  tz9.1  9724  tz9.1c  9725  tctr  9735  tcmin  9736  tcrank  9879  scottex  9880  cardlim  9967  infxpenlem  10008  infxpenc2  10017  isinfcard  10087  alephinit  10090  alephval3  10105  dfac3  10116  cflem  10241  cfval  10242  cflecard  10248  cfsuc  10252  cff1  10253  cfflb  10254  cflim2  10258  isf32lem2  10349  fin1a2lem13  10407  ac7g  10469  ttukeylem5  10508  ttukeylem7  10510  pwcfsdom  10578  pwfseqlem5  10658  pwfseq  10659  gch2  10670  winalim  10690  wunex  10734  wuncss  10740  eltskg  10745  eltsk2g  10746  gruina  10813  grur1a  10814  axgroth6  10823  swrdnd2  14605  trcleq2lem  14938  dfrtrcl2  15009  fprodss  15892  mrcflem  17550  mrcval  17554  isacs2  17597  acsfiel  17598  ipoval  18483  fpwipodrs  18493  ipodrsima  18494  mreclatBAD  18516  slwispgp  19479  pgpssslw  19482  lsmss1b  19534  lsmss2b  19536  cntzcmnss  19709  gsumzres  19777  lspf  20585  lspval  20586  lbsextlem1  20771  lbsextlem3  20773  lbsextlem4  20774  aspval  21427  mplsubglem  21558  mpllsslem  21559  basis2  22454  eltg2  22461  clsval  22541  clscld  22551  clsval2  22554  ntrcls0  22580  isnei  22607  neiint  22608  neips  22617  opnneissb  22618  opnssneib  22619  neindisj2  22627  innei  22629  neiptoptop  22635  neiptopnei  22636  neitr  22684  restcls  22685  cnpimaex  22760  cnprest2  22794  regsep  22838  nrmsep3  22859  nrmsep  22861  regsep2  22880  tgcmp  22905  uncmp  22907  bwth  22914  1stcfb  22949  1stcrest  22957  2ndcctbss  22959  1stcelcls  22965  lly1stc  23000  ssref  23016  refref  23017  comppfsc  23036  xkoopn  23093  neitx  23111  txcnp  23124  txcmplem1  23145  kqnrmlem1  23247  kqnrmlem2  23248  nrmhmph  23298  fbssfi  23341  opnfbas  23346  fbasfip  23372  fbunfip  23373  fgss2  23378  fgcl  23382  supfil  23399  isufil2  23412  filssufilg  23415  ssufl  23422  ufileu  23423  elfm3  23454  fmfnfm  23462  ufldom  23466  fbflim2  23481  flfneii  23496  flftg  23500  txflf  23510  supnfcls  23524  fclscf  23529  fclsfnflim  23531  flimfnfcls  23532  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  tsmsfbas  23632  tsmsres  23648  tsmsf1o  23649  tsmsxplem1  23657  tsmsxp  23659  ustssel  23710  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  ust0  23724  elutop  23738  ustuqtop4  23749  cfiluexsm  23795  cfiluweak  23800  blssps  23930  blss  23931  metss  24017  metrest  24033  metcnp3  24049  metnrmlem3  24377  lebnumlem3  24479  lebnum  24480  ellimc3  25396  lhop1lem  25530  dchrelbas  26739  eqscut2  27307  scutun12  27311  madebdayim  27382  madebday  27394  upgredgpr  28402  dfnbgr3  28595  nbupgr  28601  nbumgrvtx  28603  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  cusgrexilem2  28699  wlkvtxiedg  28882  wlkres  28927  upgr1wlkdlem2  29399  1pthon2v  29406  1pthon2ve  29407  cusconngr  29444  isfrgr  29513  avril1  29716  spanval  30586  spancl  30589  shsval2i  30640  omlsi  30657  ococin  30661  chsupsn  30666  pjoml  30689  shs00i  30703  chj00i  30740  chsscon3  30753  chlejb1  30765  chnle  30767  pjoml2  30864  pjoml3  30865  lecm  30870  stcltr1i  31527  mdbr  31547  dmdmd  31553  dmdi  31555  dmdbr3  31558  dmdbr4  31559  mdsl1i  31574  mdslmd1lem3  31580  mdslmd1lem4  31581  csmdsymi  31587  hatomic  31613  chrelat2  31623  atord  31641  atcvat4i  31650  fz1nntr  32015  fldgenval  32402  fldgensdrg  32404  fldgenssv  32405  fldgenssp  32408  nsgmgc  32523  nsgqusf1olem2  32525  isprmidl  32556  mxidlmax  32581  ssmxidllem  32589  ssmxidl  32590  reff  32819  cmpcref  32830  zarcls1  32849  zarclsiin  32851  zarclssn  32853  zart0  32859  zarmxt1  32860  zarcmp  32862  rhmpreimacnlem  32864  sigagenval  33138  dmsigagen  33142  sigagenss  33147  ldsysgenld  33158  ldgenpisyslem1  33161  ldgenpisyslem2  33162  dynkin  33165  carsgmon  33313  carsgclctunlem2  33318  bnj1286  34030  bnj1452  34063  fineqvac  34097  kur14lem9  34205  mclsssvlem  34553  mclsind  34561  imagesset  34925  altopthsn  34933  fnessref  35242  refssfne  35243  topjoin  35250  neifg  35256  bj-snglex  35854  bj-imdirvallem  36061  relowlssretop  36244  relowlpssretop  36245  exrecfnlem  36260  finxpreclem3  36274  pibt2  36298  poimirlem29  36517  poimir  36521  mblfinlem3  36527  totbndss  36645  heibor1lem  36677  unichnidl  36899  ispridl  36902  maxidlmax  36911  igenval  36929  igenidl  36931  igenmin  36932  igenval2  36934  brssr  37371  lsatcmp  37873  lcvexchlem4  37907  lcvexchlem5  37908  pclvalN  38761  pclclN  38762  elpcliN  38764  docaclN  39995  dihglb2  40213  doch2val2  40235  dochocss  40237  dochexmidlem7  40337  lpolconN  40358  mapdval  40499  nacsfix  41450  mzpcompact2  41490  rgspnval  41910  rgspncl  41911  rgspnmin  41913  superficl  42318  superuncl  42319  cleq2lem  42359  clcnvlem  42374  dfrtrcl3  42484  clsk1indlem2  42793  neik0pk1imk0  42798  isotone1  42799  isotone2  42800  ntrclsiso  42818  gneispacess2  42897  mnuunid  43036  mnurndlem2  43041  ssrecnpr  43067  founiiun  43875  founiiun0  43888  islptre  44335  salgenval  45037  salgenn0  45047  salgencl  45048  sssalgen  45051  salgenss  45052  salgenuni  45053  issalgend  45054  dfsalgen2  45057  salgencntex  45059  isomgreqve  46493  opndisj  47535  opnneilem  47538  sepfsepc  47560  iscnrm3rlem8  47580  iscnrm3llem2  47583  intubeu  47609  ipolubdm  47612  ipoglbdm  47615  setrec1lem1  47732  setrec1lem3  47734  setrec2fun  47737