Theorem sseq12d 3941

Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)

Hypotheses

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
sseq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
sseq12d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Proof of Theorem sseq12d

Step	Hyp	Ref	Expression
1		sseq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	sseq1d 3939	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3		sseq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	sseq2d 3940	. 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
5	2, 4	bitrd 282	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ 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:  sscon34b  4249  ssdifeq0  4441  relcnvtrgOLD  6269  sbcfung  6563  knatar  7367  suppfnss  8207  funsssuppss  8208  csbfrecsg  8303  smogt  8376  oawordri  8559  omwordi  8580  omwordri  8581  oewordi  8601  oewordri  8602  oeworde  8603  nnawordi  8631  nnmwordi  8645  nnmwordri  8646  naddssim  8696  naddss2  8701  sbthlem2  9108  sbth  9117  sbthfi  9215  marypha2lem3  9430  hartogslem1  9537  inf3lem1  9630  dfttrcl2  9726  tcrank  9902  scottabf  9940  alephle  10168  cfsmolem  10349  isfin3ds  10408  fin23lem17  10417  fin23lem39  10429  isf32lem1  10432  isf32lem2  10433  isf32lem11  10442  isf33lem  10445  isf34lem7  10458  isf34lem6  10459  fin1a2lem13  10491  itunitc1  10499  dominf  10524  dcomex  10526  axdc2lem  10527  dominfac  10659  fpwwe2cbv  10716  fpwwe2lem2  10718  fpwwe2lem4  10720  fpwwecbv  10730  fpwwelem  10731  canthwelem  10736  canthwe  10737  pwfseqlem4  10748  wunex2  10824  swrdval  14792  trcleq2lem  15145  dfrtrcl2  15216  vdwpc  17159  vdwlem1  17160  vdwlem6  17165  vdwlem7  17166  vdwlem8  17167  isstruct2  17328  ressval  17412  mreexexlemd  17819  isacs1i  17832  isssc  17996  ssc2  17998  fullfunc  18084  fthfunc  18085  isps  18743  istsr  18758  isdir  18773  gsumvalx  18866  efgi2  19940  dmdprd  20215  dprdss  20246  dmdprdpr  20266  mhpfval  22460  scmatdmat  22831  basis1  23269  baspartn  23273  eltg  23276  cncls  23593  ispnrm  23658  1stcfb  23764  2ndcctbss  23775  1stcelcls  23781  subislly  23801  kgenidm  23867  ptpjpre1  23891  txcmplem2  23962  flimval  24283  flimcf  24302  fclscf  24345  metss  24828  isngp  24916  iscph  25492  cphsscph  25573  equivcau  25622  caubl  25630  caublcls  25631  ovoliunlem3  25826  volsuplem  25877  volsup  25878  dyaddisj  25918  itg1climres  26036  addbdaylem  28404  addbday  28405  negbdaylem  28443  addonbday  28666  bdaypw2n0bndlem  28850  bdaypw2n0bnd  28851  isausgr  29746  issubgr  29853  subgrprop3  29858  cusgrfilem1  30037  wkslem1  30189  wkslem2  30190  iswlk  30192  wlkres  30250  redwlk  30252  wlkp1lem8  30260  wlkdlem2  30263  pfxwlk  30267  crctcshwlkn0lem4  30403  crctcshwlkn0lem5  30404  crctcshwlkn0lem6  30405  2wlkdlem10  30525  3wlkdlem10  30771  eupthseg  30808  issh  31811  isch  31825  hsupss  31944  shslej  31983  shlub  32017  ledi  32143  pjoi0  32320  mdbr4  32901  dmdbr4  32909  dmdi4  32910  dmdbr5  32911  mdslle1i  32920  mdslle2i  32921  mdslmd1lem1  32928  mdslmd1lem2  32929  mdslmd1lem3  32930  mdslmd1lem4  32931  mdslmd1i  32932  sumdmdlem2  33022  resvval  33933  zhmnrg  34640  ispisys  34828  cvmliftlem3  36121  ismfs  36383  nmuladdss  37037  rdgssun  38377  poimirlem32  38646  volsupnfl  38659  elrefrels2  39606  refreleq  39609  elcnvrefrels2  39622  dfsymrels2  39633  dfsymrel2  39641  elsymrels2  39645  symreleq  39650  elrefsymrels2  39661  dftrrels2  39667  dftrrel2  39669  eltrrels2  39671  trreleq  39674  eleqvrels2  39684  lssatle  40148  pmaple  40894  2polcon4bN  41051  ispautN  41232  diaord  42180  dibord  42292  dihord6apre  42389  dihord3  42390  dihord4  42391  dihcnvord  42407  dvh4dimlem  42576  islpolN  42616  mapdordlem2  42770  mapdcnvordN  42791  mapdindp  42804  hdmaplkr  43046  ismrcd1  43785  ismrcd2  43786  ismrc  43788  incssnn0  43798  diophrw  43846  hbtlem5  44206  hbt  44208  naddgeoa  44472  minregex  44611  minregex2  44612  rclexi  44691  rtrclex  44693  trclubgNEW  44694  rtrclexi  44697  cnvrcl0  44701  cnvtrcl0  44702  dfrtrcl5  44705  trcleq2lemRP  44706  trficl  44745  dfrcl2  44750  relexpss1d  44781  trclrelexplem  44787  brtrclfv2  44803  dfrtrcl3  44809  heeq12  44852  ntrk2imkb  45113  clsk3nimkb  45116  clsk1independent  45122  isotone1  45124  isotone2  45125  ntrclsss  45139  ntrclsiso  45143  ntrclsk2  45144  ntrclsk3  45146  ismnu  45321  ismnushort  45361  nzss  45377  iunincfi  46185  fourierdlem89  47281  fourierdlem90  47282  fourierdlem91  47283  meaiuninclem  47566  meaiunincf  47569  meaiuninc3v  47570  meaiuninc3  47571  meaiininclem  47572  meaiininc  47573  caragenss  47590  carageniuncllem1  47607  hoidmvle  47686  ovnhoilem2  47688  hoiqssbl  47711  ovolval5lem2  47739  vonioolem2  47767  vonicclem2  47770  isisubgr  49036  uspgrsprf  49320  scmsuppss  49559  setc1onsubc  50786