Theorem dfss2 3920

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  [wsb 2067   ∈ wcel 2111  {cab 2709   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-in 3909  df-ss 3919

This theorem is referenced by:  dfss  3921  sseqin2  4173  dfss7  4201  inabs  4216  nssinpss  4217  dfrab3ss  4273  disjssun  4418  riinn0  5031  ssex  5259  op1stb  5411  ssdmres  5962  dmressnsn  5972  sspred  6257  ordtri3or  6338  fnimaeq0  6614  f0rn0  6708  fnreseql  6981  cnvimainrn  7000  sspreima  7001  sorpssin  7664  curry1  8034  curry2  8037  tpostpos2  8177  tz7.44-2  8326  tz7.44-3  8327  frfnom  8354  ecinxp  8716  infssuni  9230  elfiun  9314  marypha1lem  9317  unxpwdom  9475  djuinf  10080  ackbij1lem16  10125  fin23lem26  10216  isf34lem7  10270  isf34lem6  10271  fpwwe2lem10  10531  fpwwe2lem12  10533  fpwwe2  10534  uzin  12772  iooval2  13278  limsupgle  15384  limsupgre  15388  bitsinv1  16353  bitsres  16384  bitsuz  16385  2prm  16603  dfphi2  16685  ressbas2  17149  ressinbas  17156  ressval3d  17157  ressress  17158  restid2  17334  xrge0base  17511  resscatc  18016  symgvalstruct  19310  pmtrmvd  19369  dprdz  19945  dprdcntz2  19953  lmhmlsp  20984  lspdisj2  21065  lidlbas  21152  ressmplbas2  21963  psdmullem  22081  difopn  22950  mretopd  23008  restcld  23088  restopnb  23091  restfpw  23095  neitr  23096  cnrest2  23202  paste  23210  isnrm2  23274  1stccnp  23378  restnlly  23398  lly1stc  23412  kgeni  23453  kgencn3  23474  ptbasfi  23497  hausdiag  23561  qtopval2  23612  qtoprest  23633  trfil2  23803  trfg  23807  uzrest  23813  trufil  23826  ufileu  23835  fclscf  23941  flimfnfcls  23944  tsmsres  24060  trust  24145  restutopopn  24154  metustfbas  24473  restmetu  24486  xrtgioo  24723  xrsmopn  24729  clsocv  25178  cmetss  25244  ovoliunlem1  25431  difmbl  25472  voliunlem1  25479  volsup2  25534  i1fima  25607  i1fima2  25608  i1fd  25610  itg1addlem5  25629  itg1climres  25643  dvmptid  25889  dvmptc  25890  dvlipcn  25927  dvlip2  25928  dvcnvrelem1  25950  dvcvx  25953  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  psercn  26364  pige3ALT  26457  dvlog  26588  dvcxp1  26677  ppiprm  27089  chtprm  27091  nolesgn2ores  27612  nogesgn1ores  27614  nodense  27632  nosupres  27647  nosupbnd2lem1  27655  noinfres  27662  noinfbnd2lem1  27670  lrrecpred  27888  onsiso  28206  bdayn0sf1o  28296  chm1i  31434  dmdsl3  32293  atssma  32356  dmdbr6ati  32401  imadifxp  32579  fnresin  32605  preimane  32650  fnpreimac  32651  mptprop  32677  df1stres  32683  df2ndres  32684  preiman0  32689  xrge00  32993  gsumhashmul  33039  cycpm2tr  33086  xrge0slmod  33311  psrbasfsupp  33570  resssra  33597  fldexttr  33669  zarcmplem  33892  esumnul  34059  esumsnf  34075  baselcarsg  34317  difelcarsg  34321  eulerpartlemgs2  34391  probmeasb  34441  ballotlemfp1  34503  signstres  34586  ftc2re  34609  bnj1322  34832  cvmscld  35315  cvmliftmolem1  35323  mrsubvrs  35564  elmsta  35590  dfon2lem4  35826  dfrdg2  35835  fvline2  36186  topbnd  36364  opnbnd  36365  neibastop1  36399  bj-disj2r  37068  bj-restsnss2  37124  bj-0int  37141  bj-prmoore  37155  bj-inexeqex  37194  bj-idreseq  37202  mblfinlem3  37705  mblfinlem4  37706  ftc1anclem6  37744  areacirclem1  37754  subspopn  37798  ssbnd  37834  heiborlem3  37859  lcvexchlem3  39081  dihglblem5aN  41337  readvrec2  42400  readvcot  42403  elrfi  42733  setindtr  43063  fnwe2lem2  43090  lmhmlnmsplit  43126  proot1hash  43234  fgraphopab  43242  tfsconcatrev  43387  insucid  43442  iunrelexp0  43741  gneispace  44173  wfaxpow  45036  restsubel  45196  uzinico2  45607  limsupval3  45736  limsupvaluz  45752  liminfval5  45809  fouriersw  46275  saliinclf  46370  saldifcl2  46372  gsumge0cl  46415  sge0sn  46423  sge0tsms  46424  sge0split  46453  caragenunidm  46552  fnresfnco  47078  fcoreslem2  47101  3f1oss1  47112  imaelsetpreimafv  47432  resinsnALT  48910  iscnrm3rlem1  48977  iscnrm3rlem4  48980  incat  49639