Theorem dfss2 3925

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3924. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3924. (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 2758	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3914	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2770	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3924	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1153	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1138	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴))
7		ancl 553	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	6, 7	impbid 215	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
9		dfbi2 479	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))))
10		pm2.21 124	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
11		pm3.4 821	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
12	10, 11	ja 188	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
13	9, 12	simplbiim 513	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
14	8, 13	impbii 212	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
15		df-clab 2744	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2848	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2848	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 643	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2130	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 279	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 341	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1842	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 278	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 307	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561   = wceq 1563  [wsb 2093   ∈ wcel 2145  {cab 2743   ∩ cin 3906   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-in 3914  df-ss 3924

This theorem is referenced by:  dfss  3926  sseqin2  4178  dfss7  4206  inabs  4221  nssinpss  4222  dfrab3ss  4278  disjssun  4425  riinn0  5044  ssex  5281  op1stb  5443  ssdmres  6002  dmressnsn  6012  sspred  6300  ordtri3or  6382  fnimaeq0  6658  f0rn0  6753  fnreseql  7033  cnvimainrn  7052  sspreima  7053  sorpssin  7718  curry1  8087  curry2  8090  tpostpos2  8231  tz7.44-2  8382  tz7.44-3  8383  frfnom  8410  ecinxp  8778  infssuni  9291  elfiun  9378  marypha1lem  9381  unxpwdom  9539  djuinf  10160  ackbij1lem16  10205  fin23lem26  10297  isf34lem7  10351  isf34lem6  10352  fpwwe2lem10  10613  fpwwe2lem12  10615  fpwwe2  10616  uzin  12886  iooval2  13393  limsupgle  15516  limsupgre  15520  bitsinv1  16488  bitsres  16519  bitsuz  16520  2prm  16738  dfphi2  16821  ressbas2  17286  ressinbas  17293  ressval3d  17294  ressress  17295  restid2  17471  xrge0base  17649  resscatc  18154  symgvalstruct  19455  pmtrmvd  19514  dprdz  20090  dprdcntz2  20098  lmhmlsp  21136  lspdisj2  21217  lidlbas  21305  ressmplbas2  22134  psdmullem  22285  difopn  23148  mretopd  23206  restcld  23286  restopnb  23289  restfpw  23293  neitr  23294  cnrest2  23400  paste  23408  isnrm2  23472  1stccnp  23576  restnlly  23596  lly1stc  23610  kgeni  23651  kgencn3  23672  ptbasfi  23695  hausdiag  23759  qtopval2  23810  qtoprest  23831  trfil2  24001  trfg  24005  uzrest  24011  trufil  24024  ufileu  24033  fclscf  24139  flimfnfcls  24142  tsmsres  24258  trust  24343  restutopopn  24352  metustfbas  24671  restmetu  24684  xrtgioo  24921  xrsmopn  24927  clsocv  25366  cmetss  25432  ovoliunlem1  25618  difmbl  25659  voliunlem1  25666  volsup2  25721  i1fima  25794  i1fima2  25795  i1fd  25797  itg1addlem5  25816  itg1climres  25830  dvmptid  26073  dvmptc  26074  dvlipcn  26110  dvlip2  26111  dvcnvrelem1  26133  dvcvx  26136  taylthlem1  26490  taylthlem2  26491  psercn  26543  pige3ALT  26639  dvlog  26770  dvcxp1  26859  ppiprm  27269  chtprm  27271  nolesgn2ores  27790  nogesgn1ores  27792  nodense  27810  nosupres  27825  nosupbnd2lem1  27833  noinfres  27840  noinfbnd2lem1  27848  lrrecpred  28091  oniso  28418  bdayn0sf1o  28517  chm1i  31713  dmdsl3  32572  atssma  32635  dmdbr6ati  32680  imadifxp  32852  fnresin  32877  preimane  32922  fnpreimac  32923  mptprop  32951  df1stres  32957  df2ndres  32958  preiman0  32963  xrge00  33242  gsumhashmul  33295  cycpm2tr  33347  xrge0slmod  33578  psrbasfsupp  33813  resssra  33889  fldexttr  33960  zarcmplem  34183  esumnul  34350  esumsnf  34366  baselcarsg  34608  difelcarsg  34612  eulerpartlemgs2  34682  probmeasb  34732  ballotlemfp1  34794  signstres  34874  ftc2re  34897  bnj1322  35122  cvmscld  35631  cvmliftmolem1  35639  mrsubvrs  35880  elmsta  35906  dfon2lem4  36142  dfrdg2  36151  fvline2  36504  topbnd  36692  opnbnd  36693  neibastop1  36727  ttcwf2  36893  dfttc4  36898  bj-disj2r  37520  bj-restsnss2  37581  bj-0int  37598  bj-prmoore  37612  bj-inexeqex  37653  bj-idreseq  37661  mblfinlem3  38165  mblfinlem4  38166  ftc1anclem6  38204  areacirclem1  38214  subspopn  38258  ssbnd  38294  heiborlem3  38319  lcvexchlem3  39667  dihglblem5aN  41923  readvrec2  42977  readvcot  42980  elrfi  43282  setindtr  43608  fnwe2lem2  43635  lmhmlnmsplit  43671  proot1hash  43779  fgraphopab  43787  tfsconcatrev  43932  insucid  43987  iunrelexp0  44285  gneispace  44717  wfaxpow  45565  restsubel  45730  uzinico2  46136  limsupval3  46265  limsupvaluz  46281  liminfval5  46338  fouriersw  46804  saliinclf  46899  saldifcl2  46901  gsumge0cl  46944  sge0sn  46952  sge0tsms  46953  sge0split  46982  caragenunidm  47081  fnresfnco  47634  fcoreslem2  47657  3f1oss1  47668  imaelsetpreimafv  48000  resinsnALT  49503  iscnrm3rlem1  49570  iscnrm3rlem4  49573  incat  50231