Theorem dfss2 3921

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3920. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3920. (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 3910	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2742	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3920	. . 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 3902   ⊆ wss 3903

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 3910  df-ss 3920

This theorem is referenced by:  dfss  3922  sseqin2  4177  dfss7  4205  inabs  4220  nssinpss  4221  dfrab3ss  4277  disjssun  4422  riinn0  5040  ssex  5268  op1stb  5427  ssdmres  5980  dmressnsn  5990  sspred  6276  ordtri3or  6357  fnimaeq0  6633  f0rn0  6727  fnreseql  7002  cnvimainrn  7021  sspreima  7022  sorpssin  7686  curry1  8056  curry2  8059  tpostpos2  8199  tz7.44-2  8348  tz7.44-3  8349  frfnom  8376  ecinxp  8741  infssuni  9258  elfiun  9345  marypha1lem  9348  unxpwdom  9506  djuinf  10111  ackbij1lem16  10156  fin23lem26  10247  isf34lem7  10301  isf34lem6  10302  fpwwe2lem10  10563  fpwwe2lem12  10565  fpwwe2  10566  uzin  12799  iooval2  13306  limsupgle  15412  limsupgre  15416  bitsinv1  16381  bitsres  16412  bitsuz  16413  2prm  16631  dfphi2  16713  ressbas2  17177  ressinbas  17184  ressval3d  17185  ressress  17186  restid2  17362  xrge0base  17540  resscatc  18045  symgvalstruct  19338  pmtrmvd  19397  dprdz  19973  dprdcntz2  19981  lmhmlsp  21013  lspdisj2  21094  lidlbas  21181  ressmplbas2  21994  psdmullem  22120  difopn  22990  mretopd  23048  restcld  23128  restopnb  23131  restfpw  23135  neitr  23136  cnrest2  23242  paste  23250  isnrm2  23314  1stccnp  23418  restnlly  23438  lly1stc  23452  kgeni  23493  kgencn3  23514  ptbasfi  23537  hausdiag  23601  qtopval2  23652  qtoprest  23673  trfil2  23843  trfg  23847  uzrest  23853  trufil  23866  ufileu  23875  fclscf  23981  flimfnfcls  23984  tsmsres  24100  trust  24185  restutopopn  24194  metustfbas  24513  restmetu  24526  xrtgioo  24763  xrsmopn  24769  clsocv  25218  cmetss  25284  ovoliunlem1  25471  difmbl  25512  voliunlem1  25519  volsup2  25574  i1fima  25647  i1fima2  25648  i1fd  25650  itg1addlem5  25669  itg1climres  25683  dvmptid  25929  dvmptc  25930  dvlipcn  25967  dvlip2  25968  dvcnvrelem1  25990  dvcvx  25993  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  psercn  26404  pige3ALT  26497  dvlog  26628  dvcxp1  26717  ppiprm  27129  chtprm  27131  nolesgn2ores  27652  nogesgn1ores  27654  nodense  27672  nosupres  27687  nosupbnd2lem1  27695  noinfres  27702  noinfbnd2lem1  27710  lrrecpred  27952  oniso  28279  bdayn0sf1o  28378  chm1i  31543  dmdsl3  32402  atssma  32465  dmdbr6ati  32510  imadifxp  32687  fnresin  32713  preimane  32758  fnpreimac  32759  mptprop  32787  df1stres  32793  df2ndres  32794  preiman0  32799  xrge00  33106  gsumhashmul  33160  cycpm2tr  33212  xrge0slmod  33440  psrbasfsupp  33704  resssra  33763  fldexttr  33835  zarcmplem  34058  esumnul  34225  esumsnf  34241  baselcarsg  34483  difelcarsg  34487  eulerpartlemgs2  34557  probmeasb  34607  ballotlemfp1  34669  signstres  34752  ftc2re  34775  bnj1322  34997  cvmscld  35486  cvmliftmolem1  35494  mrsubvrs  35735  elmsta  35761  dfon2lem4  35997  dfrdg2  36006  fvline2  36359  topbnd  36537  opnbnd  36538  neibastop1  36572  bj-disj2r  37273  bj-restsnss2  37334  bj-0int  37351  bj-prmoore  37365  bj-inexeqex  37406  bj-idreseq  37414  mblfinlem3  37907  mblfinlem4  37908  ftc1anclem6  37946  areacirclem1  37956  subspopn  38000  ssbnd  38036  heiborlem3  38061  lcvexchlem3  39409  dihglblem5aN  41665  readvrec2  42728  readvcot  42731  elrfi  43048  setindtr  43378  fnwe2lem2  43405  lmhmlnmsplit  43441  proot1hash  43549  fgraphopab  43557  tfsconcatrev  43702  insucid  43757  iunrelexp0  44055  gneispace  44487  wfaxpow  45350  restsubel  45509  uzinico2  45918  limsupval3  46047  limsupvaluz  46063  liminfval5  46120  fouriersw  46586  saliinclf  46681  saldifcl2  46683  gsumge0cl  46726  sge0sn  46734  sge0tsms  46735  sge0split  46764  caragenunidm  46863  fnresfnco  47398  fcoreslem2  47421  3f1oss1  47432  imaelsetpreimafv  47752  resinsnALT  49229  iscnrm3rlem1  49296  iscnrm3rlem4  49299  incat  49957