Theorem dfss2 3924

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3923. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3923. (Revised by GG, 15-May-2025.)

Assertion

Ref	Expression
dfss2	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Proof of Theorem dfss2

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2758	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3913	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2770	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3923	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1155	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1140	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴))
7		ancl 554	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	6, 7	impbid 215	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
9		dfbi2 480	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))))
10		pm2.21 124	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
11		pm3.4 822	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
12	10, 11	ja 188	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
13	9, 12	simplbiim 514	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
14	8, 13	impbii 212	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
15		df-clab 2744	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2848	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2848	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 644	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2131	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 279	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 341	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 278	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 307	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  [wsb 2099   ∈ wcel 2146  {cab 2743   ∩ cin 3905   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-in 3913  df-ss 3923

This theorem is used by:  dfss  3925  sseqin2  4176  dfss7  4204  inabs  4219  nssinpss  4220  dfrab3ss  4276  disjssun  4428  riinn0  5051  ssexg  5292  ssexOLD  5294  op1stb  5455  ssdmres  6014  dmressnsn  6024  sspred  6315  ordtri3or  6397  fnimaeq0  6672  f0rn0  6767  fnreseql  7047  cnvimainrn  7066  sspreima  7067  sorpssin  7734  curry1  8101  curry2  8104  tpostpos2  8245  tz7.44-2  8396  tz7.44-3  8397  frfnom  8424  ecinxp  8792  infssuni  9306  elfiun  9393  marypha1lem  9396  unxpwdom  9554  djuinf  10184  ackbij1lem16  10229  fin23lem26  10320  isf34lem7  10374  isf34lem6  10375  fpwwe2lem10  10636  fpwwe2lem12  10638  fpwwe2  10639  uzin  12909  iooval2  13416  limsupgle  15547  limsupgre  15551  bitsinv1  16517  bitsres  16548  bitsuz  16549  2prm  16767  dfphi2  16850  ressbas2  17315  ressinbas  17322  ressval3d  17323  ressress  17324  restid2  17500  xrge0base  17678  resscatc  18183  symgvalstruct  19490  pmtrmvd  19549  dprdz  20125  dprdcntz2  20133  lmhmlsp  21199  lspdisj2  21280  lidlbas  21368  ressmplbas2  22206  psdmullem  22357  difopn  23220  mretopd  23278  restcld  23358  restopnb  23361  restfpw  23365  neitr  23366  cnrest2  23472  paste  23480  isnrm2  23544  1stccnp  23648  restnlly  23668  lly1stc  23682  kgeni  23723  kgencn3  23744  ptbasfi  23767  hausdiag  23831  qtopval2  23882  qtoprest  23903  trfil2  24073  trfg  24077  uzrest  24083  trufil  24096  ufileu  24105  fclscf  24211  flimfnfcls  24214  tsmsres  24330  trust  24415  restutopopn  24424  metustfbas  24743  restmetu  24756  xrtgioo  24993  xrsmopn  24999  clsocv  25438  cmetss  25504  ovoliunlem1  25690  difmbl  25731  voliunlem1  25738  volsup2  25793  i1fima  25866  i1fima2  25867  i1fd  25869  itg1addlem5  25888  itg1climres  25902  dvmptid  26145  dvmptc  26146  dvlipcn  26182  dvlip2  26183  dvcnvrelem1  26205  dvcvx  26208  taylthlem1  26565  taylthlem2  26566  psercn  26618  pige3ALT  26714  dvlog  26845  dvcxp1  26934  ppiprm  27344  chtprm  27346  nolesgn2ores  27865  nogesgn1ores  27867  nodense  27885  nosupres  27900  nosupbnd2lem1  27908  noinfres  27915  noinfbnd2lem1  27923  lrrecpred  28166  oniso  28493  bdayn0sf1o  28592  chm1i  31837  dmdsl3  32696  atssma  32759  dmdbr6ati  32804  imadifxp  32975  fnresin  32998  preimane  33043  fnpreimac  33044  mptprop  33072  df1stres  33078  df2ndres  33079  preiman0  33084  xrge00  33357  gsumhashmul  33410  cycpm2tr  33462  xrge0slmod  33691  psrbasfsupp  33924  resssra  34000  fldexttr  34071  zarcmplem  34294  esumnul  34461  esumsnf  34477  baselcarsg  34720  difelcarsg  34724  eulerpartlemgs2  34794  probmeasb  34844  ballotlemfp1  34906  signstres  34986  ftc2re  35009  bnj1322  35234  cvmscld  35778  cvmliftmolem1  35786  mrsubvrs  36027  elmsta  36053  dfon2lem4  36289  dfrdg2  36298  fvline2  36651  topbnd  36868  opnbnd  36869  neibastop1  36903  ttcwf2  37069  dfttc4  37074  bj-disj2r  37697  bj-restsnss2  37759  bj-0int  37776  bj-prmoore  37790  bj-inexeqex  37831  bj-idreseq  37839  mblfinlem3  38343  mblfinlem4  38344  ftc1anclem6  38382  areacirclem1  38392  subspopn  38436  ssbnd  38472  heiborlem3  38497  lcvexchlem3  39843  dihglblem5aN  42099  readvrec2  43155  readvcot  43158  elrfi  43458  setindtr  43784  fnwe2lem2  43811  lmhmlnmsplit  43847  proot1hash  43955  fgraphopab  43963  tfsconcatrev  44108  insucid  44163  iunrelexp0  44461  gneispace  44893  wfaxpow  45739  restsubel  45904  uzinico2  46310  limsupval3  46439  limsupvaluz  46455  liminfval5  46512  fouriersw  46978  saliinclf  47073  saldifcl2  47075  gsumge0cl  47118  sge0sn  47126  sge0tsms  47127  sge0split  47156  caragenunidm  47255  fnresfnco  47811  fcoreslem2  47834  3f1oss1  47845  imaelsetpreimafv  48177  resinsnALT  49684  iscnrm3rlem1  49751  iscnrm3rlem4  49754  incat  50412