Theorem dfss2 3976

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3975. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3975. (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 2722	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3965	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2734	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3975	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1134	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1119	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴))
7		ancl 543	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	6, 7	impbid 211	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
9		dfbi2 473	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))))
10		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
11		pm3.4 808	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
12	10, 11	ja 186	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
13	9, 12	simplbiim 503	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
14	8, 13	impbii 208	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
15		df-clab 2707	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2812	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2812	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 630	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2089	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 275	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 337	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 274	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1814	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 274	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1532   = wceq 1534  [wsb 2061   ∈ wcel 2100  {cab 2706   ∩ cin 3957   ⊆ wss 3958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-in 3965  df-ss 3975

This theorem is referenced by:  dfss  3977  sseqin2  4224  dfss7  4250  inabs  4265  nssinpss  4266  dfrab3ss  4323  disjssun  4473  riinn0  5094  ssex  5327  op1stb  5479  ssdmres  6025  dmressnsn  6035  sspred  6324  ordtri3or  6410  fnimaeq0  6696  f0rn0  6789  fnreseql  7063  cnvimainrn  7082  sspreima  7083  sorpssin  7744  curry1  8123  curry2  8126  tpostpos2  8266  tz7.44-2  8441  tz7.44-3  8442  frfnom  8469  ecinxp  8825  infssuni  9389  elfiun  9474  marypha1lem  9477  unxpwdom  9633  djuinf  10233  ackbij1lem16  10278  fin23lem26  10369  isf34lem7  10423  isf34lem6  10424  fpwwe2lem10  10684  fpwwe2lem12  10686  fpwwe2  10687  uzin  12918  iooval2  13415  limsupgle  15492  limsupgre  15496  bitsinv1  16455  bitsres  16486  bitsuz  16487  2prm  16706  dfphi2  16789  ressbas2  17264  ressinbas  17272  ressval3d  17273  ressval3dOLD  17274  ressress  17275  restid2  17458  resscatc  18144  symgvalstruct  19406  symgvalstructOLD  19407  pmtrmvd  19466  dprdz  20042  dprdcntz2  20050  lmhmlsp  21039  lspdisj2  21120  lidlbas  21215  ressmplbas2  22035  psdmullem  22158  difopn  23029  mretopd  23087  restcld  23167  restopnb  23170  restfpw  23174  neitr  23175  cnrest2  23281  paste  23289  isnrm2  23353  1stccnp  23457  restnlly  23477  lly1stc  23491  kgeni  23532  kgencn3  23553  ptbasfi  23576  hausdiag  23640  qtopval2  23691  qtoprest  23712  trfil2  23882  trfg  23886  uzrest  23892  trufil  23905  ufileu  23914  fclscf  24020  flimfnfcls  24023  tsmsres  24139  trust  24225  restutopopn  24234  metustfbas  24557  restmetu  24570  xrtgioo  24813  xrsmopn  24819  clsocv  25269  cmetss  25335  ovoliunlem1  25522  difmbl  25563  voliunlem1  25570  volsup2  25625  i1fima  25698  i1fima2  25699  i1fd  25701  itg1addlem5  25721  itg1climres  25735  dvmptid  25980  dvmptc  25981  dvlipcn  26018  dvlip2  26019  dvcnvrelem1  26041  dvcvx  26044  taylthlem1  26398  taylthlem2  26399  taylthlem2OLD  26400  psercn  26453  pige3ALT  26544  dvlog  26675  dvcxp1  26764  ppiprm  27176  chtprm  27178  nolesgn2ores  27699  nogesgn1ores  27701  nodense  27719  nosupres  27734  nosupbnd2lem1  27742  noinfres  27749  noinfbnd2lem1  27757  lrrecpred  27955  chm1i  31431  dmdsl3  32290  atssma  32353  dmdbr6ati  32398  imadifxp  32567  fnresin  32589  preimane  32633  fnpreimac  32634  mptprop  32655  df1stres  32660  df2ndres  32661  preiman0  32666  xrge0base  32942  xrge00  32943  gsumhashmul  32985  cycpm2tr  33057  xrge0slmod  33286  resssra  33547  fldexttr  33616  zarcmplem  33772  esumnul  33957  esumsnf  33973  baselcarsg  34216  difelcarsg  34220  eulerpartlemgs2  34290  probmeasb  34340  ballotlemfp1  34401  signstres  34497  ftc2re  34520  bnj1322  34743  cvmscld  35186  cvmliftmolem1  35194  mrsubvrs  35435  elmsta  35461  dfon2lem4  35695  dfrdg2  35704  fvline2  36055  topbnd  36122  opnbnd  36123  neibastop1  36157  bj-disj2r  36820  bj-restsnss2  36876  bj-0int  36893  bj-prmoore  36907  bj-inexeqex  36946  bj-idreseq  36954  mblfinlem3  37445  mblfinlem4  37446  ftc1anclem6  37484  areacirclem1  37494  subspopn  37538  ssbnd  37574  heiborlem3  37599  lcvexchlem3  38819  dihglblem5aN  41076  elrfi  42463  setindtr  42794  fnwe2lem2  42824  lmhmlnmsplit  42860  proot1hash  42972  fgraphopab  42980  tfsconcatrev  43126  insucid  43182  iunrelexp0  43481  gneispace  43913  restsubel  44869  uzinico2  45291  limsupval3  45424  limsupvaluz  45440  liminfval5  45497  fouriersw  45963  saliinclf  46058  saldifcl2  46060  gsumge0cl  46103  sge0sn  46111  sge0tsms  46112  sge0split  46141  caragenunidm  46240  fnresfnco  46767  fcoreslem2  46790  imaelsetpreimafv  47078  iscnrm3rlem1  48396  iscnrm3rlem4  48399