Theorem dfss2 3932

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  [wsb 2065   ∈ wcel 2109  {cab 2707   ∩ cin 3913   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-in 3921  df-ss 3931

This theorem is referenced by:  dfss  3933  sseqin2  4186  dfss7  4214  inabs  4229  nssinpss  4230  dfrab3ss  4286  disjssun  4431  riinn0  5047  ssex  5276  op1stb  5431  ssdmres  5984  dmressnsn  5994  sspred  6283  ordtri3or  6364  fnimaeq0  6651  f0rn0  6745  fnreseql  7020  cnvimainrn  7039  sspreima  7040  sorpssin  7707  curry1  8083  curry2  8086  tpostpos2  8226  tz7.44-2  8375  tz7.44-3  8376  frfnom  8403  ecinxp  8765  infssuni  9297  elfiun  9381  marypha1lem  9384  unxpwdom  9542  djuinf  10142  ackbij1lem16  10187  fin23lem26  10278  isf34lem7  10332  isf34lem6  10333  fpwwe2lem10  10593  fpwwe2lem12  10595  fpwwe2  10596  uzin  12833  iooval2  13339  limsupgle  15443  limsupgre  15447  bitsinv1  16412  bitsres  16443  bitsuz  16444  2prm  16662  dfphi2  16744  ressbas2  17208  ressinbas  17215  ressval3d  17216  ressress  17217  restid2  17393  resscatc  18071  symgvalstruct  19327  pmtrmvd  19386  dprdz  19962  dprdcntz2  19970  lmhmlsp  20956  lspdisj2  21037  lidlbas  21124  ressmplbas2  21934  psdmullem  22052  difopn  22921  mretopd  22979  restcld  23059  restopnb  23062  restfpw  23066  neitr  23067  cnrest2  23173  paste  23181  isnrm2  23245  1stccnp  23349  restnlly  23369  lly1stc  23383  kgeni  23424  kgencn3  23445  ptbasfi  23468  hausdiag  23532  qtopval2  23583  qtoprest  23604  trfil2  23774  trfg  23778  uzrest  23784  trufil  23797  ufileu  23806  fclscf  23912  flimfnfcls  23915  tsmsres  24031  trust  24117  restutopopn  24126  metustfbas  24445  restmetu  24458  xrtgioo  24695  xrsmopn  24701  clsocv  25150  cmetss  25216  ovoliunlem1  25403  difmbl  25444  voliunlem1  25451  volsup2  25506  i1fima  25579  i1fima2  25580  i1fd  25582  itg1addlem5  25601  itg1climres  25615  dvmptid  25861  dvmptc  25862  dvlipcn  25899  dvlip2  25900  dvcnvrelem1  25922  dvcvx  25925  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  psercn  26336  pige3ALT  26429  dvlog  26560  dvcxp1  26649  ppiprm  27061  chtprm  27063  nolesgn2ores  27584  nogesgn1ores  27586  nodense  27604  nosupres  27619  nosupbnd2lem1  27627  noinfres  27634  noinfbnd2lem1  27642  lrrecpred  27851  onsiso  28169  bdayn0sf1o  28259  chm1i  31385  dmdsl3  32244  atssma  32307  dmdbr6ati  32352  imadifxp  32530  fnresin  32550  preimane  32594  fnpreimac  32595  mptprop  32621  df1stres  32627  df2ndres  32628  preiman0  32633  xrge0base  32952  xrge00  32953  gsumhashmul  33001  cycpm2tr  33076  xrge0slmod  33319  resssra  33583  fldexttr  33654  zarcmplem  33871  esumnul  34038  esumsnf  34054  baselcarsg  34297  difelcarsg  34301  eulerpartlemgs2  34371  probmeasb  34421  ballotlemfp1  34483  signstres  34566  ftc2re  34589  bnj1322  34812  cvmscld  35260  cvmliftmolem1  35268  mrsubvrs  35509  elmsta  35535  dfon2lem4  35774  dfrdg2  35783  fvline2  36134  topbnd  36312  opnbnd  36313  neibastop1  36347  bj-disj2r  37016  bj-restsnss2  37072  bj-0int  37089  bj-prmoore  37103  bj-inexeqex  37142  bj-idreseq  37150  mblfinlem3  37653  mblfinlem4  37654  ftc1anclem6  37692  areacirclem1  37702  subspopn  37746  ssbnd  37782  heiborlem3  37807  lcvexchlem3  39029  dihglblem5aN  41286  readvrec2  42349  readvcot  42352  elrfi  42682  setindtr  43013  fnwe2lem2  43040  lmhmlnmsplit  43076  proot1hash  43184  fgraphopab  43192  tfsconcatrev  43337  insucid  43392  iunrelexp0  43691  gneispace  44123  wfaxpow  44987  restsubel  45147  uzinico2  45559  limsupval3  45690  limsupvaluz  45706  liminfval5  45763  fouriersw  46229  saliinclf  46324  saldifcl2  46326  gsumge0cl  46369  sge0sn  46377  sge0tsms  46378  sge0split  46407  caragenunidm  46506  fnresfnco  47042  fcoreslem2  47065  3f1oss1  47076  imaelsetpreimafv  47396  resinsnALT  48861  iscnrm3rlem1  48928  iscnrm3rlem4  48931  incat  49590