Theorem dfss2 3908

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3907. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3907. (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 2733	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3897	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2745	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3907	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1143	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1128	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴))
7		ancl 549	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	6, 7	impbid 213	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
9		dfbi2 475	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))))
10		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
11		pm3.4 815	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
12	10, 11	ja 187	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
13	9, 12	simplbiim 509	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
14	8, 13	impbii 210	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
15		df-clab 2719	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2823	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2823	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 638	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2104	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 277	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 339	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 276	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1826	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 276	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 305	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547  [wsb 2073   ∈ wcel 2119  {cab 2718   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-in 3897  df-ss 3907

This theorem is referenced by:  dfss  3909  sseqin2  4159  dfss7  4186  inabs  4201  nssinpss  4202  dfrab3ss  4258  disjssun  4403  riinn0  5019  ssex  5256  op1stb  5418  ssdmres  5972  dmressnsn  5982  sspred  6268  ordtri3or  6349  fnimaeq0  6625  f0rn0  6719  fnreseql  6996  cnvimainrn  7015  sspreima  7016  sorpssin  7681  curry1  8050  curry2  8053  tpostpos2  8194  tz7.44-2  8343  tz7.44-3  8344  frfnom  8371  ecinxp  8736  infssuni  9253  elfiun  9340  marypha1lem  9343  unxpwdom  9501  djuinf  10109  ackbij1lem16  10154  fin23lem26  10245  isf34lem7  10299  isf34lem6  10300  fpwwe2lem10  10561  fpwwe2lem12  10563  fpwwe2  10564  uzin  12822  iooval2  13329  limsupgle  15437  limsupgre  15441  bitsinv1  16409  bitsres  16440  bitsuz  16441  2prm  16659  dfphi2  16742  ressbas2  17206  ressinbas  17213  ressval3d  17214  ressress  17215  restid2  17391  xrge0base  17569  resscatc  18074  symgvalstruct  19370  pmtrmvd  19429  dprdz  20005  dprdcntz2  20013  lmhmlsp  21046  lspdisj2  21127  lidlbas  21214  ressmplbas2  22009  psdmullem  22160  difopn  23024  mretopd  23082  restcld  23162  restopnb  23165  restfpw  23169  neitr  23170  cnrest2  23276  paste  23284  isnrm2  23348  1stccnp  23452  restnlly  23472  lly1stc  23486  kgeni  23527  kgencn3  23548  ptbasfi  23571  hausdiag  23635  qtopval2  23686  qtoprest  23707  trfil2  23877  trfg  23881  uzrest  23887  trufil  23900  ufileu  23909  fclscf  24015  flimfnfcls  24018  tsmsres  24134  trust  24219  restutopopn  24228  metustfbas  24547  restmetu  24560  xrtgioo  24797  xrsmopn  24803  clsocv  25242  cmetss  25308  ovoliunlem1  25494  difmbl  25535  voliunlem1  25542  volsup2  25597  i1fima  25670  i1fima2  25671  i1fd  25673  itg1addlem5  25692  itg1climres  25706  dvmptid  25949  dvmptc  25950  dvlipcn  25986  dvlip2  25987  dvcnvrelem1  26009  dvcvx  26012  taylthlem1  26363  taylthlem2  26364  psercn  26416  pige3ALT  26509  dvlog  26640  dvcxp1  26729  ppiprm  27139  chtprm  27141  nolesgn2ores  27661  nogesgn1ores  27663  nodense  27681  nosupres  27696  nosupbnd2lem1  27704  noinfres  27711  noinfbnd2lem1  27719  lrrecpred  27961  oniso  28288  bdayn0sf1o  28387  chm1i  31552  dmdsl3  32411  atssma  32474  dmdbr6ati  32519  imadifxp  32697  fnresin  32723  preimane  32768  fnpreimac  32769  mptprop  32797  df1stres  32803  df2ndres  32804  preiman0  32809  xrge00  33100  gsumhashmul  33155  cycpm2tr  33207  xrge0slmod  33438  psrbasfsupp  33702  resssra  33778  fldexttr  33849  zarcmplem  34072  esumnul  34239  esumsnf  34255  baselcarsg  34497  difelcarsg  34501  eulerpartlemgs2  34571  probmeasb  34621  ballotlemfp1  34683  signstres  34766  ftc2re  34789  bnj1322  35011  cvmscld  35508  cvmliftmolem1  35516  mrsubvrs  35757  elmsta  35783  dfon2lem4  36019  dfrdg2  36028  fvline2  36381  topbnd  36559  opnbnd  36560  neibastop1  36594  ttcwf2  36760  dfttc4  36765  bj-disj2r  37388  bj-restsnss2  37449  bj-0int  37466  bj-prmoore  37480  bj-inexeqex  37521  bj-idreseq  37529  mblfinlem3  38033  mblfinlem4  38034  ftc1anclem6  38072  areacirclem1  38082  subspopn  38126  ssbnd  38162  heiborlem3  38187  lcvexchlem3  39535  dihglblem5aN  41791  readvrec2  42845  readvcot  42848  elrfi  43150  setindtr  43476  fnwe2lem2  43503  lmhmlnmsplit  43539  proot1hash  43647  fgraphopab  43655  tfsconcatrev  43800  insucid  43855  iunrelexp0  44153  gneispace  44585  wfaxpow  45448  restsubel  45607  uzinico2  46013  limsupval3  46142  limsupvaluz  46158  liminfval5  46215  fouriersw  46681  saliinclf  46776  saldifcl2  46778  gsumge0cl  46821  sge0sn  46829  sge0tsms  46830  sge0split  46859  caragenunidm  46958  fnresfnco  47511  fcoreslem2  47534  3f1oss1  47545  imaelsetpreimafv  47877  resinsnALT  49370  iscnrm3rlem1  49437  iscnrm3rlem4  49440  incat  50098