Theorem dfss2 3919

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3918. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3918. (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 2729	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3908	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2741	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3918	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1137	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1122	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴))
7		ancl 544	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	6, 7	impbid 212	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
9		dfbi2 474	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))))
10		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
11		pm3.4 809	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
12	10, 11	ja 186	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
13	9, 12	simplbiim 504	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
14	8, 13	impbii 209	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
15		df-clab 2715	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2819	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2819	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 632	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2098	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 276	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 338	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 275	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 275	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 304	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  [wsb 2067   ∈ wcel 2113  {cab 2714   ∩ cin 3900   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-in 3908  df-ss 3918

This theorem is referenced by:  dfss  3920  sseqin2  4175  dfss7  4203  inabs  4218  nssinpss  4219  dfrab3ss  4275  disjssun  4420  riinn0  5038  ssex  5266  op1stb  5419  ssdmres  5972  dmressnsn  5982  sspred  6268  ordtri3or  6349  fnimaeq0  6625  f0rn0  6719  fnreseql  6993  cnvimainrn  7012  sspreima  7013  sorpssin  7676  curry1  8046  curry2  8049  tpostpos2  8189  tz7.44-2  8338  tz7.44-3  8339  frfnom  8366  ecinxp  8729  infssuni  9246  elfiun  9333  marypha1lem  9336  unxpwdom  9494  djuinf  10099  ackbij1lem16  10144  fin23lem26  10235  isf34lem7  10289  isf34lem6  10290  fpwwe2lem10  10551  fpwwe2lem12  10553  fpwwe2  10554  uzin  12787  iooval2  13294  limsupgle  15400  limsupgre  15404  bitsinv1  16369  bitsres  16400  bitsuz  16401  2prm  16619  dfphi2  16701  ressbas2  17165  ressinbas  17172  ressval3d  17173  ressress  17174  restid2  17350  xrge0base  17528  resscatc  18033  symgvalstruct  19326  pmtrmvd  19385  dprdz  19961  dprdcntz2  19969  lmhmlsp  21001  lspdisj2  21082  lidlbas  21169  ressmplbas2  21982  psdmullem  22108  difopn  22978  mretopd  23036  restcld  23116  restopnb  23119  restfpw  23123  neitr  23124  cnrest2  23230  paste  23238  isnrm2  23302  1stccnp  23406  restnlly  23426  lly1stc  23440  kgeni  23481  kgencn3  23502  ptbasfi  23525  hausdiag  23589  qtopval2  23640  qtoprest  23661  trfil2  23831  trfg  23835  uzrest  23841  trufil  23854  ufileu  23863  fclscf  23969  flimfnfcls  23972  tsmsres  24088  trust  24173  restutopopn  24182  metustfbas  24501  restmetu  24514  xrtgioo  24751  xrsmopn  24757  clsocv  25206  cmetss  25272  ovoliunlem1  25459  difmbl  25500  voliunlem1  25507  volsup2  25562  i1fima  25635  i1fima2  25636  i1fd  25638  itg1addlem5  25657  itg1climres  25671  dvmptid  25917  dvmptc  25918  dvlipcn  25955  dvlip2  25956  dvcnvrelem1  25978  dvcvx  25981  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  psercn  26392  pige3ALT  26485  dvlog  26616  dvcxp1  26705  ppiprm  27117  chtprm  27119  nolesgn2ores  27640  nogesgn1ores  27642  nodense  27660  nosupres  27675  nosupbnd2lem1  27683  noinfres  27690  noinfbnd2lem1  27698  lrrecpred  27940  oniso  28267  bdayn0sf1o  28366  chm1i  31531  dmdsl3  32390  atssma  32453  dmdbr6ati  32498  imadifxp  32676  fnresin  32702  preimane  32748  fnpreimac  32749  mptprop  32777  df1stres  32783  df2ndres  32784  preiman0  32789  xrge00  33096  gsumhashmul  33150  cycpm2tr  33201  xrge0slmod  33429  psrbasfsupp  33693  resssra  33743  fldexttr  33815  zarcmplem  34038  esumnul  34205  esumsnf  34221  baselcarsg  34463  difelcarsg  34467  eulerpartlemgs2  34537  probmeasb  34587  ballotlemfp1  34649  signstres  34732  ftc2re  34755  bnj1322  34978  cvmscld  35467  cvmliftmolem1  35475  mrsubvrs  35716  elmsta  35742  dfon2lem4  35978  dfrdg2  35987  fvline2  36340  topbnd  36518  opnbnd  36519  neibastop1  36553  bj-disj2r  37229  bj-restsnss2  37289  bj-0int  37306  bj-prmoore  37320  bj-inexeqex  37359  bj-idreseq  37367  mblfinlem3  37860  mblfinlem4  37861  ftc1anclem6  37899  areacirclem1  37909  subspopn  37953  ssbnd  37989  heiborlem3  38014  lcvexchlem3  39296  dihglblem5aN  41552  readvrec2  42616  readvcot  42619  elrfi  42936  setindtr  43266  fnwe2lem2  43293  lmhmlnmsplit  43329  proot1hash  43437  fgraphopab  43445  tfsconcatrev  43590  insucid  43645  iunrelexp0  43943  gneispace  44375  wfaxpow  45238  restsubel  45397  uzinico2  45807  limsupval3  45936  limsupvaluz  45952  liminfval5  46009  fouriersw  46475  saliinclf  46570  saldifcl2  46572  gsumge0cl  46615  sge0sn  46623  sge0tsms  46624  sge0split  46653  caragenunidm  46752  fnresfnco  47287  fcoreslem2  47310  3f1oss1  47321  imaelsetpreimafv  47641  resinsnALT  49118  iscnrm3rlem1  49185  iscnrm3rlem4  49188  incat  49846