Theorem eqssd 2079

Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22.

Hypotheses

Ref	Expression
eqssd.1	|- (ph -> A (_ B)
eqssd.2	|- (ph -> B (_ A)

Assertion

Ref	Expression
eqssd	|- (ph -> A = B)

Proof of Theorem eqssd

Step	Hyp	Ref	Expression
1		eqssd.1	. . 3 |- (ph -> A (_ B)
2		eqssd.2	. . 3 |- (ph -> B (_ A)
3	1, 2	jca 288	. 2 |- (ph -> (A (_ B /\ B (_ A))
4		eqss 2077	. 2 |- (A = B <-> (A (_ B /\ B (_ A))
5	3, 4	sylibr 200	1 |- (ph -> A = B)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   (_ wss 2047

This theorem is referenced by:  difsn 2464  sspr 2475  unissel 2527  int0el 2561  tz7.7 2973  onint 3006  relfld 3515  fimacnv 3810  oaass 4195  odi 4210  omass 4211  oelim2 4222  oaabslem 4251  mapenlem2 4490  r1val1 4658  rankr1 4674  rankr1id 4697  rankc2 4706  rankxplim 4712  oncard 4829  distrpr 5132  ltexpri 5149  reclem4pr 5159  infxpidmlem7 7558  tgtopt 7628  basgen2t 7639  2basgent 7641  clslp 7748  cncnplem4 7777  cnconst 7780  uniopn 7861  unirnbl 7875  bcthlem10 8008  grplactf1o 8098  ubthlem5 8533  psdmrn 8648  ococint 9297  chsupsn 9312  chabs1t 9439  spansncv 9597  mdslj1 10246  mdslj2 10247  atoml 10309  atcvatlem 10312  atcvat3 10323  sumdmdlem 10345  rdmob 10681  rcmob 10682

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain