Theorem dfss2 3994

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537  [wsb 2064   ∈ wcel 2108  {cab 2717   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-in 3983  df-ss 3993

This theorem is referenced by:  dfss  3995  sseqin2  4244  dfss7  4270  inabs  4285  nssinpss  4286  dfrab3ss  4342  disjssun  4491  riinn0  5106  ssex  5339  op1stb  5491  ssdmres  6042  dmressnsn  6052  sspred  6341  ordtri3or  6427  fnimaeq0  6713  f0rn0  6806  fnreseql  7081  cnvimainrn  7100  sspreima  7101  sorpssin  7766  curry1  8145  curry2  8148  tpostpos2  8288  tz7.44-2  8463  tz7.44-3  8464  frfnom  8491  ecinxp  8850  infssuni  9414  elfiun  9499  marypha1lem  9502  unxpwdom  9658  djuinf  10258  ackbij1lem16  10303  fin23lem26  10394  isf34lem7  10448  isf34lem6  10449  fpwwe2lem10  10709  fpwwe2lem12  10711  fpwwe2  10712  uzin  12943  iooval2  13440  limsupgle  15523  limsupgre  15527  bitsinv1  16488  bitsres  16519  bitsuz  16520  2prm  16739  dfphi2  16821  ressbas2  17296  ressinbas  17304  ressval3d  17305  ressval3dOLD  17306  ressress  17307  restid2  17490  resscatc  18176  symgvalstruct  19438  symgvalstructOLD  19439  pmtrmvd  19498  dprdz  20074  dprdcntz2  20082  lmhmlsp  21071  lspdisj2  21152  lidlbas  21247  ressmplbas2  22068  psdmullem  22192  difopn  23063  mretopd  23121  restcld  23201  restopnb  23204  restfpw  23208  neitr  23209  cnrest2  23315  paste  23323  isnrm2  23387  1stccnp  23491  restnlly  23511  lly1stc  23525  kgeni  23566  kgencn3  23587  ptbasfi  23610  hausdiag  23674  qtopval2  23725  qtoprest  23746  trfil2  23916  trfg  23920  uzrest  23926  trufil  23939  ufileu  23948  fclscf  24054  flimfnfcls  24057  tsmsres  24173  trust  24259  restutopopn  24268  metustfbas  24591  restmetu  24604  xrtgioo  24847  xrsmopn  24853  clsocv  25303  cmetss  25369  ovoliunlem1  25556  difmbl  25597  voliunlem1  25604  volsup2  25659  i1fima  25732  i1fima2  25733  i1fd  25735  itg1addlem5  25755  itg1climres  25769  dvmptid  26015  dvmptc  26016  dvlipcn  26053  dvlip2  26054  dvcnvrelem1  26076  dvcvx  26079  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  psercn  26488  pige3ALT  26580  dvlog  26711  dvcxp1  26800  ppiprm  27212  chtprm  27214  nolesgn2ores  27735  nogesgn1ores  27737  nodense  27755  nosupres  27770  nosupbnd2lem1  27778  noinfres  27785  noinfbnd2lem1  27793  lrrecpred  27995  chm1i  31488  dmdsl3  32347  atssma  32410  dmdbr6ati  32455  imadifxp  32623  fnresin  32645  preimane  32688  fnpreimac  32689  mptprop  32710  df1stres  32715  df2ndres  32716  preiman0  32721  xrge0base  32997  xrge00  32998  gsumhashmul  33040  cycpm2tr  33112  xrge0slmod  33341  resssra  33602  fldexttr  33671  zarcmplem  33827  esumnul  34012  esumsnf  34028  baselcarsg  34271  difelcarsg  34275  eulerpartlemgs2  34345  probmeasb  34395  ballotlemfp1  34456  signstres  34552  ftc2re  34575  bnj1322  34798  cvmscld  35241  cvmliftmolem1  35249  mrsubvrs  35490  elmsta  35516  dfon2lem4  35750  dfrdg2  35759  fvline2  36110  topbnd  36290  opnbnd  36291  neibastop1  36325  bj-disj2r  36994  bj-restsnss2  37050  bj-0int  37067  bj-prmoore  37081  bj-inexeqex  37120  bj-idreseq  37128  mblfinlem3  37619  mblfinlem4  37620  ftc1anclem6  37658  areacirclem1  37668  subspopn  37712  ssbnd  37748  heiborlem3  37773  lcvexchlem3  38992  dihglblem5aN  41249  elrfi  42650  setindtr  42981  fnwe2lem2  43008  lmhmlnmsplit  43044  proot1hash  43156  fgraphopab  43164  tfsconcatrev  43310  insucid  43365  iunrelexp0  43664  gneispace  44096  restsubel  45058  uzinico2  45480  limsupval3  45613  limsupvaluz  45629  liminfval5  45686  fouriersw  46152  saliinclf  46247  saldifcl2  46249  gsumge0cl  46292  sge0sn  46300  sge0tsms  46301  sge0split  46330  caragenunidm  46429  fnresfnco  46956  fcoreslem2  46979  3f1oss1  46990  imaelsetpreimafv  47269  iscnrm3rlem1  48620  iscnrm3rlem4  48623