Theorem dfss2 3980

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3979. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3979. (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 2727	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3969	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2739	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3979	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1136	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1121	. . . . . . 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 2712	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2821	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2821	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 632	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2090	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 276	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 338	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 275	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1815	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 275	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 304	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536  [wsb 2061   ∈ wcel 2105  {cab 2711   ∩ cin 3961   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-in 3969  df-ss 3979

This theorem is referenced by:  dfss  3981  sseqin2  4230  dfss7  4256  inabs  4271  nssinpss  4272  dfrab3ss  4328  disjssun  4473  riinn0  5087  ssex  5326  op1stb  5481  ssdmres  6032  dmressnsn  6042  sspred  6331  ordtri3or  6417  fnimaeq0  6701  f0rn0  6793  fnreseql  7067  cnvimainrn  7086  sspreima  7087  sorpssin  7749  curry1  8127  curry2  8130  tpostpos2  8270  tz7.44-2  8445  tz7.44-3  8446  frfnom  8473  ecinxp  8830  infssuni  9383  elfiun  9467  marypha1lem  9470  unxpwdom  9626  djuinf  10226  ackbij1lem16  10271  fin23lem26  10362  isf34lem7  10416  isf34lem6  10417  fpwwe2lem10  10677  fpwwe2lem12  10679  fpwwe2  10680  uzin  12915  iooval2  13416  limsupgle  15509  limsupgre  15513  bitsinv1  16475  bitsres  16506  bitsuz  16507  2prm  16725  dfphi2  16807  ressbas2  17282  ressinbas  17290  ressval3d  17291  ressval3dOLD  17292  ressress  17293  restid2  17476  resscatc  18162  symgvalstruct  19428  symgvalstructOLD  19429  pmtrmvd  19488  dprdz  20064  dprdcntz2  20072  lmhmlsp  21065  lspdisj2  21146  lidlbas  21241  ressmplbas2  22062  psdmullem  22186  difopn  23057  mretopd  23115  restcld  23195  restopnb  23198  restfpw  23202  neitr  23203  cnrest2  23309  paste  23317  isnrm2  23381  1stccnp  23485  restnlly  23505  lly1stc  23519  kgeni  23560  kgencn3  23581  ptbasfi  23604  hausdiag  23668  qtopval2  23719  qtoprest  23740  trfil2  23910  trfg  23914  uzrest  23920  trufil  23933  ufileu  23942  fclscf  24048  flimfnfcls  24051  tsmsres  24167  trust  24253  restutopopn  24262  metustfbas  24585  restmetu  24598  xrtgioo  24841  xrsmopn  24847  clsocv  25297  cmetss  25363  ovoliunlem1  25550  difmbl  25591  voliunlem1  25598  volsup2  25653  i1fima  25726  i1fima2  25727  i1fd  25729  itg1addlem5  25749  itg1climres  25763  dvmptid  26009  dvmptc  26010  dvlipcn  26047  dvlip2  26048  dvcnvrelem1  26070  dvcvx  26073  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  psercn  26484  pige3ALT  26576  dvlog  26707  dvcxp1  26796  ppiprm  27208  chtprm  27210  nolesgn2ores  27731  nogesgn1ores  27733  nodense  27751  nosupres  27766  nosupbnd2lem1  27774  noinfres  27781  noinfbnd2lem1  27789  lrrecpred  27991  chm1i  31484  dmdsl3  32343  atssma  32406  dmdbr6ati  32451  imadifxp  32620  fnresin  32642  preimane  32686  fnpreimac  32687  mptprop  32712  df1stres  32718  df2ndres  32719  preiman0  32724  xrge0base  32998  xrge00  32999  gsumhashmul  33046  cycpm2tr  33121  xrge0slmod  33355  resssra  33616  fldexttr  33685  zarcmplem  33841  esumnul  34028  esumsnf  34044  baselcarsg  34287  difelcarsg  34291  eulerpartlemgs2  34361  probmeasb  34411  ballotlemfp1  34472  signstres  34568  ftc2re  34591  bnj1322  34814  cvmscld  35257  cvmliftmolem1  35265  mrsubvrs  35506  elmsta  35532  dfon2lem4  35767  dfrdg2  35776  fvline2  36127  topbnd  36306  opnbnd  36307  neibastop1  36341  bj-disj2r  37010  bj-restsnss2  37066  bj-0int  37083  bj-prmoore  37097  bj-inexeqex  37136  bj-idreseq  37144  mblfinlem3  37645  mblfinlem4  37646  ftc1anclem6  37684  areacirclem1  37694  subspopn  37738  ssbnd  37774  heiborlem3  37799  lcvexchlem3  39017  dihglblem5aN  41274  readvrec2  42369  elrfi  42681  setindtr  43012  fnwe2lem2  43039  lmhmlnmsplit  43075  proot1hash  43183  fgraphopab  43191  tfsconcatrev  43337  insucid  43392  iunrelexp0  43691  gneispace  44123  restsubel  45095  uzinico2  45514  limsupval3  45647  limsupvaluz  45663  liminfval5  45720  fouriersw  46186  saliinclf  46281  saldifcl2  46283  gsumge0cl  46326  sge0sn  46334  sge0tsms  46335  sge0split  46364  caragenunidm  46463  fnresfnco  46990  fcoreslem2  47013  3f1oss1  47024  imaelsetpreimafv  47319  iscnrm3rlem1  48736  iscnrm3rlem4  48739