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  37285  bj-0int  37302  bj-prmoore  37316  bj-inexeqex  37355  bj-idreseq  37363  mblfinlem3  37856  mblfinlem4  37857  ftc1anclem6  37895  areacirclem1  37905  subspopn  37949  ssbnd  37985  heiborlem3  38010  lcvexchlem3  39292  dihglblem5aN  41548  readvrec2  42612  readvcot  42615  elrfi  42932  setindtr  43262  fnwe2lem2  43289  lmhmlnmsplit  43325  proot1hash  43433  fgraphopab  43441  tfsconcatrev  43586  insucid  43641  iunrelexp0  43939  gneispace  44371  wfaxpow  45234  restsubel  45393  uzinico2  45803  limsupval3  45932  limsupvaluz  45948  liminfval5  46005  fouriersw  46471  saliinclf  46566  saldifcl2  46568  gsumge0cl  46611  sge0sn  46619  sge0tsms  46620  sge0split  46649  caragenunidm  46748  fnresfnco  47283  fcoreslem2  47306  3f1oss1  47317  imaelsetpreimafv  47637  resinsnALT  49114  iscnrm3rlem1  49181  iscnrm3rlem4  49184  incat  49842