Theorem dfss2 4097

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3901. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3901. (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 2756	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 4094	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2768	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3901	. . 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 2742	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2847	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2847	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 644	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2133	. . . . . . 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 2101   ∈ wcel 2147  {cab 2741   ⊆ wss 3900   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-in 4094

This theorem is used by:  dfss  4098  sseqin2  4123  dfss7  4151  inabs  4214  nssinpss  4215  dfrab3ss  4271  disjssun  4424  riinn0  5046  ssexg  5286  ssexOLD  5288  op1stb  5445  ssdmres  6019  dmressnsn  6028  sspred  6337  ordtri3or  6419  fnimaeq0  6700  f0rn0  6795  fnreseql  7076  cnvimainrn  7096  sspreima  7097  sorpssin  7777  curry1  8150  curry2  8153  tpostpos2  8300  tz7.44-2  8451  tz7.44-3  8452  frfnom  8479  ecinxp  8849  infssuni  9371  elfiun  9457  marypha1lem  9460  unxpwdom  9618  djuinf  10304  ackbij1lem16  10349  fin23lem26  10440  isf34lem7  10494  isf34lem6  10495  fpwwe2lem10  10762  fpwwe2lem12  10764  fpwwe2  10765  uzin  13039  iooval2  13547  limsupgle  15685  limsupgre  15689  bitsinv1  16653  bitsres  16684  bitsuz  16685  2prm  16908  dfphi2  16992  ressbas2  17457  ressinbas  17464  ressval3d  17465  ressress  17466  restid2  17642  xrge0base  17820  resscatc  18325  symgvalstruct  19653  pmtrmvd  19712  dprdz  20288  dprdcntz2  20296  lmhmlsp  21366  lspdisj2  21447  lidlbas  21535  ressmplbas2  22379  psdmullem  22530  difopn  23396  mretopd  23454  restcld  23534  restopnb  23537  restfpw  23541  neitr  23542  cnrest2  23648  paste  23656  isnrm2  23720  1stccnp  23825  restnlly  23845  lly1stc  23859  kgeni  23900  kgencn3  23921  ptbasfi  23944  hausdiag  24008  qtopval2  24059  qtoprest  24080  trfil2  24250  trfg  24254  uzrest  24260  trufil  24273  ufileu  24282  fclscf  24388  flimfnfcls  24391  tsmsres  24507  trust  24592  restutopopn  24601  metustfbas  24920  restmetu  24933  xrtgioo  25170  xrsmopn  25176  clsocv  25615  cmetss  25681  ovoliunlem1  25867  difmbl  25908  voliunlem1  25915  volsup2  25970  i1fima  26043  i1fima2  26044  i1fd  26046  itg1addlem5  26065  itg1climres  26079  dvmptid  26321  dvmptc  26322  dvlipcn  26358  dvlip2  26359  dvcnvrelem1  26381  dvcvx  26384  taylthlem1  26746  taylthlem2  26747  psercn  26799  pige3ALT  26894  dvlog  27025  dvcxp1  27114  ppiprm  27524  chtprm  27526  nolesgn2ores  28075  nogesgn1ores  28077  nodense  28095  nosupres  28110  nosupbnd2lem1  28118  noinfres  28125  noinfbnd2lem1  28133  lrrecpred  28376  oniso  28703  bdayn0sf1o  28802  chm1i  32104  dmdsl3  32963  atssma  33026  dmdbr6ati  33071  imadifxp  33283  fnresin  33306  preimane  33351  fnpreimac  33352  mptprop  33378  df1stres  33384  df2ndres  33385  preiman0  33390  xrge00  33664  gsumhashmul  33717  cycpm2tr  33769  xrge0slmod  34006  psrbasfsupp  34247  resssra  34323  fldexttr  34394  zarcmplem  34617  esumnul  34784  esumsnf  34800  baselcarsg  35042  difelcarsg  35046  eulerpartlemgs2  35116  probmeasb  35166  ballotlemfp1  35228  signstres  35308  ftc2re  35331  bnj1322  35556  cvmscld  36239  cvmliftmolem1  36247  mrsubvrs  36488  elmsta  36514  dfon2lem4  36756  dfrdg2  36765  fvline2  37119  topbnd  37320  opnbnd  37321  neibastop1  37355  ttcwf2  37521  dfttc4  37526  bj-disj2r  38149  bj-resssxp  38176  bj-restsnss2  38268  bj-0int  38285  bj-prmoore  38299  bj-inexeqex  38336  bj-idreseq  38344  mblfinlem3  38838  mblfinlem4  38839  ftc1anclem6  38877  areacirclem1  38887  subspopn  38945  ssbnd  38981  heiborlem3  39006  lcvexchlem3  40352  dihglblem5aN  42608  readvrec2  43672  readvcot  43675  elrfi  43965  setindtr  44291  lmhmlnmsplit  44349  proot1hash  44452  fgraphopab  44460  tfsconcatrev  44605  insucid  44660  iunrelexp0  44957  gneispace  45389  wfaxpow  46245  restsubel  46435  uzinico2  46840  limsupval3  46969  limsupvaluz  46985  liminfval5  47042  fouriersw  47508  saliinclf  47603  saldifcl2  47605  gsumge0cl  47648  sge0sn  47656  sge0tsms  47657  sge0split  47686  caragenunidm  47785  fnresfnco  48378  fcoreslem2  48401  3f1oss1  48412  imaelsetpreimafv  48744  resinsnALT  50311  iscnrm3rlem1  50379  iscnrm3rlem4  50382  incat  51064  parhomco2  51085  parhomco  51086  parcatid2  51088  parcatid  51089  parmapco2  51097  parmapco  51098