Theorem dfss2 3920

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3919. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3919. (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 3909	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2766	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3919	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1149	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1134	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴))
7		ancl 552	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	6, 7	impbid 214	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
9		dfbi2 478	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))))
10		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
11		pm3.4 819	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
12	10, 11	ja 187	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
13	9, 12	simplbiim 512	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
14	8, 13	impbii 211	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
15		df-clab 2740	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2844	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2844	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 641	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2126	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 278	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 340	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 277	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1838	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 277	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   = wceq 1559  [wsb 2089   ∈ wcel 2141  {cab 2739   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-in 3909  df-ss 3919

This theorem is referenced by:  dfss  3921  sseqin2  4173  dfss7  4201  inabs  4216  nssinpss  4217  dfrab3ss  4273  disjssun  4419  riinn0  5037  ssex  5274  op1stb  5436  ssdmres  5995  dmressnsn  6005  sspred  6291  ordtri3or  6372  fnimaeq0  6648  f0rn0  6743  fnreseql  7023  cnvimainrn  7042  sspreima  7043  sorpssin  7708  curry1  8076  curry2  8079  tpostpos2  8220  tz7.44-2  8371  tz7.44-3  8372  frfnom  8399  ecinxp  8767  infssuni  9282  elfiun  9369  marypha1lem  9372  unxpwdom  9530  djuinf  10138  ackbij1lem16  10183  fin23lem26  10275  isf34lem7  10329  isf34lem6  10330  fpwwe2lem10  10591  fpwwe2lem12  10593  fpwwe2  10594  uzin  12868  iooval2  13375  limsupgle  15494  limsupgre  15498  bitsinv1  16466  bitsres  16497  bitsuz  16498  2prm  16716  dfphi2  16799  ressbas2  17264  ressinbas  17271  ressval3d  17272  ressress  17273  restid2  17449  xrge0base  17627  resscatc  18132  symgvalstruct  19427  pmtrmvd  19486  dprdz  20062  dprdcntz2  20070  lmhmlsp  21103  lspdisj2  21184  lidlbas  21271  ressmplbas2  22066  psdmullem  22217  difopn  23081  mretopd  23139  restcld  23219  restopnb  23222  restfpw  23226  neitr  23227  cnrest2  23333  paste  23341  isnrm2  23405  1stccnp  23509  restnlly  23529  lly1stc  23543  kgeni  23584  kgencn3  23605  ptbasfi  23628  hausdiag  23692  qtopval2  23743  qtoprest  23764  trfil2  23934  trfg  23938  uzrest  23944  trufil  23957  ufileu  23966  fclscf  24072  flimfnfcls  24075  tsmsres  24191  trust  24276  restutopopn  24285  metustfbas  24604  restmetu  24617  xrtgioo  24854  xrsmopn  24860  clsocv  25299  cmetss  25365  ovoliunlem1  25551  difmbl  25592  voliunlem1  25599  volsup2  25654  i1fima  25727  i1fima2  25728  i1fd  25730  itg1addlem5  25749  itg1climres  25763  dvmptid  26006  dvmptc  26007  dvlipcn  26043  dvlip2  26044  dvcnvrelem1  26066  dvcvx  26069  taylthlem1  26423  taylthlem2  26424  psercn  26476  pige3ALT  26572  dvlog  26703  dvcxp1  26792  ppiprm  27202  chtprm  27204  nolesgn2ores  27723  nogesgn1ores  27725  nodense  27743  nosupres  27758  nosupbnd2lem1  27766  noinfres  27773  noinfbnd2lem1  27781  lrrecpred  28024  oniso  28351  bdayn0sf1o  28450  chm1i  31615  dmdsl3  32474  atssma  32537  dmdbr6ati  32582  imadifxp  32760  fnresin  32786  preimane  32831  fnpreimac  32832  mptprop  32860  df1stres  32866  df2ndres  32867  preiman0  32872  xrge00  33152  gsumhashmul  33207  cycpm2tr  33259  xrge0slmod  33494  psrbasfsupp  33768  resssra  33844  fldexttr  33915  zarcmplem  34138  esumnul  34305  esumsnf  34321  baselcarsg  34563  difelcarsg  34567  eulerpartlemgs2  34637  probmeasb  34687  ballotlemfp1  34749  signstres  34829  ftc2re  34852  bnj1322  35077  cvmscld  35583  cvmliftmolem1  35591  mrsubvrs  35832  elmsta  35858  dfon2lem4  36094  dfrdg2  36103  fvline2  36456  topbnd  36644  opnbnd  36645  neibastop1  36679  ttcwf2  36845  dfttc4  36850  bj-disj2r  37473  bj-restsnss2  37534  bj-0int  37551  bj-prmoore  37565  bj-inexeqex  37606  bj-idreseq  37614  mblfinlem3  38118  mblfinlem4  38119  ftc1anclem6  38157  areacirclem1  38167  subspopn  38211  ssbnd  38247  heiborlem3  38272  lcvexchlem3  39620  dihglblem5aN  41876  readvrec2  42930  readvcot  42933  elrfi  43235  setindtr  43561  fnwe2lem2  43588  lmhmlnmsplit  43624  proot1hash  43732  fgraphopab  43740  tfsconcatrev  43885  insucid  43940  iunrelexp0  44238  gneispace  44670  wfaxpow  45533  restsubel  45691  uzinico2  46097  limsupval3  46226  limsupvaluz  46242  liminfval5  46299  fouriersw  46765  saliinclf  46860  saldifcl2  46862  gsumge0cl  46905  sge0sn  46913  sge0tsms  46914  sge0split  46943  caragenunidm  47042  fnresfnco  47595  fcoreslem2  47618  3f1oss1  47629  imaelsetpreimafv  47961  resinsnALT  49454  iscnrm3rlem1  49521  iscnrm3rlem4  49524  incat  50182