Theorem dfss2 3917

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3916. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3916. (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 2754	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3906	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2766	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3916	. . 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 2740	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2844	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2844	. . . . . . . . 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 2145  {cab 2739   ∩ cin 3898   ⊆ wss 3899

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-in 3906  df-ss 3916

This theorem is used by:  dfss  3918  sseqin2  4169  dfss7  4197  inabs  4212  nssinpss  4213  dfrab3ss  4269  disjssun  4421  riinn0  5043  ssexg  5281  ssexOLD  5283  op1stb  5440  ssdmres  6004  dmressnsn  6012  sspred  6312  ordtri3or  6394  fnimaeq0  6670  f0rn0  6765  fnreseql  7045  cnvimainrn  7064  sspreima  7065  sorpssin  7745  curry1  8113  curry2  8116  tpostpos2  8257  tz7.44-2  8408  tz7.44-3  8409  frfnom  8436  ecinxp  8806  infssuni  9328  elfiun  9415  marypha1lem  9418  unxpwdom  9576  djuinf  10260  ackbij1lem16  10305  fin23lem26  10396  isf34lem7  10450  isf34lem6  10451  fpwwe2lem10  10718  fpwwe2lem12  10720  fpwwe2  10721  uzin  12994  iooval2  13502  limsupgle  15637  limsupgre  15641  bitsinv1  16605  bitsres  16636  bitsuz  16637  2prm  16860  dfphi2  16944  ressbas2  17409  ressinbas  17416  ressval3d  17417  ressress  17418  restid2  17594  xrge0base  17772  resscatc  18277  symgvalstruct  19604  pmtrmvd  19663  dprdz  20239  dprdcntz2  20247  lmhmlsp  21317  lspdisj2  21398  lidlbas  21486  ressmplbas2  22328  psdmullem  22479  difopn  23345  mretopd  23403  restcld  23483  restopnb  23486  restfpw  23490  neitr  23491  cnrest2  23597  paste  23605  isnrm2  23669  1stccnp  23774  restnlly  23794  lly1stc  23808  kgeni  23849  kgencn3  23870  ptbasfi  23893  hausdiag  23957  qtopval2  24008  qtoprest  24029  trfil2  24199  trfg  24203  uzrest  24209  trufil  24222  ufileu  24231  fclscf  24337  flimfnfcls  24340  tsmsres  24456  trust  24541  restutopopn  24550  metustfbas  24869  restmetu  24882  xrtgioo  25119  xrsmopn  25125  clsocv  25564  cmetss  25630  ovoliunlem1  25816  difmbl  25857  voliunlem1  25864  volsup2  25919  i1fima  25992  i1fima2  25993  i1fd  25995  itg1addlem5  26014  itg1climres  26028  dvmptid  26270  dvmptc  26271  dvlipcn  26307  dvlip2  26308  dvcnvrelem1  26330  dvcvx  26333  taylthlem1  26693  taylthlem2  26694  psercn  26746  pige3ALT  26841  dvlog  26972  dvcxp1  27061  ppiprm  27471  chtprm  27473  nolesgn2ores  28022  nogesgn1ores  28024  nodense  28042  nosupres  28057  nosupbnd2lem1  28065  noinfres  28072  noinfbnd2lem1  28080  lrrecpred  28323  oniso  28650  bdayn0sf1o  28749  chm1i  32051  dmdsl3  32910  atssma  32973  dmdbr6ati  33018  imadifxp  33188  fnresin  33211  preimane  33256  fnpreimac  33257  mptprop  33284  df1stres  33290  df2ndres  33291  preiman0  33296  xrge00  33568  gsumhashmul  33621  cycpm2tr  33673  xrge0slmod  33902  psrbasfsupp  34136  resssra  34212  fldexttr  34283  zarcmplem  34506  esumnul  34673  esumsnf  34689  baselcarsg  34931  difelcarsg  34935  eulerpartlemgs2  35005  probmeasb  35055  ballotlemfp1  35117  signstres  35197  ftc2re  35220  bnj1322  35445  cvmscld  36017  cvmliftmolem1  36025  mrsubvrs  36266  elmsta  36292  dfon2lem4  36528  dfrdg2  36537  fvline2  36891  topbnd  37092  opnbnd  37093  neibastop1  37127  ttcwf2  37293  dfttc4  37298  bj-disj2r  37921  bj-restsnss2  37985  bj-0int  38002  bj-prmoore  38016  bj-inexeqex  38055  bj-idreseq  38063  mblfinlem3  38557  mblfinlem4  38558  ftc1anclem6  38596  areacirclem1  38606  subspopn  38666  ssbnd  38702  heiborlem3  38727  lcvexchlem3  40073  dihglblem5aN  42329  readvrec2  43392  readvcot  43395  elrfi  43684  setindtr  44010  fnwe2lem2  44037  lmhmlnmsplit  44073  proot1hash  44181  fgraphopab  44189  tfsconcatrev  44334  insucid  44389  iunrelexp0  44687  gneispace  45119  wfaxpow  45965  restsubel  46137  uzinico2  46542  limsupval3  46671  limsupvaluz  46687  liminfval5  46744  fouriersw  47210  saliinclf  47305  saldifcl2  47307  gsumge0cl  47350  sge0sn  47358  sge0tsms  47359  sge0split  47388  caragenunidm  47487  fnresfnco  48080  fcoreslem2  48103  3f1oss1  48114  imaelsetpreimafv  48446  resinsnALT  49950  iscnrm3rlem1  50017  iscnrm3rlem4  50020  incat  50678