Theorem dfss2 3908

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  [wsb 2068   ∈ wcel 2114  {cab 2715   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-in 3897  df-ss 3907

This theorem is referenced by:  dfss  3909  sseqin2  4164  dfss7  4192  inabs  4207  nssinpss  4208  dfrab3ss  4264  disjssun  4409  riinn0  5026  ssex  5258  op1stb  5419  ssdmres  5972  dmressnsn  5982  sspred  6268  ordtri3or  6349  fnimaeq0  6625  f0rn0  6719  fnreseql  6994  cnvimainrn  7013  sspreima  7014  sorpssin  7678  curry1  8047  curry2  8050  tpostpos2  8190  tz7.44-2  8339  tz7.44-3  8340  frfnom  8367  ecinxp  8732  infssuni  9249  elfiun  9336  marypha1lem  9339  unxpwdom  9497  djuinf  10102  ackbij1lem16  10147  fin23lem26  10238  isf34lem7  10292  isf34lem6  10293  fpwwe2lem10  10554  fpwwe2lem12  10556  fpwwe2  10557  uzin  12815  iooval2  13322  limsupgle  15430  limsupgre  15434  bitsinv1  16402  bitsres  16433  bitsuz  16434  2prm  16652  dfphi2  16735  ressbas2  17199  ressinbas  17206  ressval3d  17207  ressress  17208  restid2  17384  xrge0base  17562  resscatc  18067  symgvalstruct  19363  pmtrmvd  19422  dprdz  19998  dprdcntz2  20006  lmhmlsp  21036  lspdisj2  21117  lidlbas  21204  ressmplbas2  22015  psdmullem  22141  difopn  23009  mretopd  23067  restcld  23147  restopnb  23150  restfpw  23154  neitr  23155  cnrest2  23261  paste  23269  isnrm2  23333  1stccnp  23437  restnlly  23457  lly1stc  23471  kgeni  23512  kgencn3  23533  ptbasfi  23556  hausdiag  23620  qtopval2  23671  qtoprest  23692  trfil2  23862  trfg  23866  uzrest  23872  trufil  23885  ufileu  23894  fclscf  24000  flimfnfcls  24003  tsmsres  24119  trust  24204  restutopopn  24213  metustfbas  24532  restmetu  24545  xrtgioo  24782  xrsmopn  24788  clsocv  25227  cmetss  25293  ovoliunlem1  25479  difmbl  25520  voliunlem1  25527  volsup2  25582  i1fima  25655  i1fima2  25656  i1fd  25658  itg1addlem5  25677  itg1climres  25691  dvmptid  25934  dvmptc  25935  dvlipcn  25971  dvlip2  25972  dvcnvrelem1  25994  dvcvx  25997  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  psercn  26404  pige3ALT  26497  dvlog  26628  dvcxp1  26717  ppiprm  27128  chtprm  27130  nolesgn2ores  27650  nogesgn1ores  27652  nodense  27670  nosupres  27685  nosupbnd2lem1  27693  noinfres  27700  noinfbnd2lem1  27708  lrrecpred  27950  oniso  28277  bdayn0sf1o  28376  chm1i  31542  dmdsl3  32401  atssma  32464  dmdbr6ati  32509  imadifxp  32686  fnresin  32712  preimane  32757  fnpreimac  32758  mptprop  32786  df1stres  32792  df2ndres  32793  preiman0  32798  xrge00  33089  gsumhashmul  33143  cycpm2tr  33195  xrge0slmod  33423  psrbasfsupp  33687  resssra  33746  fldexttr  33818  zarcmplem  34041  esumnul  34208  esumsnf  34224  baselcarsg  34466  difelcarsg  34470  eulerpartlemgs2  34540  probmeasb  34590  ballotlemfp1  34652  signstres  34735  ftc2re  34758  bnj1322  34980  cvmscld  35471  cvmliftmolem1  35479  mrsubvrs  35720  elmsta  35746  dfon2lem4  35982  dfrdg2  35991  fvline2  36344  topbnd  36522  opnbnd  36523  neibastop1  36557  ttcwf2  36723  dfttc4  36728  bj-disj2r  37351  bj-restsnss2  37412  bj-0int  37429  bj-prmoore  37443  bj-inexeqex  37484  bj-idreseq  37492  mblfinlem3  37994  mblfinlem4  37995  ftc1anclem6  38033  areacirclem1  38043  subspopn  38087  ssbnd  38123  heiborlem3  38148  lcvexchlem3  39496  dihglblem5aN  41752  readvrec2  42807  readvcot  42810  elrfi  43140  setindtr  43470  fnwe2lem2  43497  lmhmlnmsplit  43533  proot1hash  43641  fgraphopab  43649  tfsconcatrev  43794  insucid  43849  iunrelexp0  44147  gneispace  44579  wfaxpow  45442  restsubel  45601  uzinico2  46009  limsupval3  46138  limsupvaluz  46154  liminfval5  46211  fouriersw  46677  saliinclf  46772  saldifcl2  46774  gsumge0cl  46817  sge0sn  46825  sge0tsms  46826  sge0split  46855  caragenunidm  46954  fnresfnco  47501  fcoreslem2  47524  3f1oss1  47535  imaelsetpreimafv  47867  resinsnALT  49360  iscnrm3rlem1  49427  iscnrm3rlem4  49430  incat  50088