Theorem dfss2 3949

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3948. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3948. (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 2729	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3938	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2741	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3948	. . 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 2715	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2818	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2818	. . . . . . . . 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 2714   ∩ cin 3930   ⊆ wss 3931

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-in 3938  df-ss 3948

This theorem is referenced by:  dfss  3950  sseqin2  4203  dfss7  4231  inabs  4246  nssinpss  4247  dfrab3ss  4303  disjssun  4448  riinn0  5064  ssex  5296  op1stb  5451  ssdmres  6005  dmressnsn  6015  sspred  6304  ordtri3or  6389  fnimaeq0  6676  f0rn0  6768  fnreseql  7043  cnvimainrn  7062  sspreima  7063  sorpssin  7730  curry1  8108  curry2  8111  tpostpos2  8251  tz7.44-2  8426  tz7.44-3  8427  frfnom  8454  ecinxp  8811  infssuni  9363  elfiun  9447  marypha1lem  9450  unxpwdom  9608  djuinf  10208  ackbij1lem16  10253  fin23lem26  10344  isf34lem7  10398  isf34lem6  10399  fpwwe2lem10  10659  fpwwe2lem12  10661  fpwwe2  10662  uzin  12897  iooval2  13400  limsupgle  15498  limsupgre  15502  bitsinv1  16466  bitsres  16497  bitsuz  16498  2prm  16716  dfphi2  16798  ressbas2  17264  ressinbas  17271  ressval3d  17272  ressress  17273  restid2  17449  resscatc  18127  symgvalstruct  19383  pmtrmvd  19442  dprdz  20018  dprdcntz2  20026  lmhmlsp  21012  lspdisj2  21093  lidlbas  21180  ressmplbas2  21990  psdmullem  22108  difopn  22977  mretopd  23035  restcld  23115  restopnb  23118  restfpw  23122  neitr  23123  cnrest2  23229  paste  23237  isnrm2  23301  1stccnp  23405  restnlly  23425  lly1stc  23439  kgeni  23480  kgencn3  23501  ptbasfi  23524  hausdiag  23588  qtopval2  23639  qtoprest  23660  trfil2  23830  trfg  23834  uzrest  23840  trufil  23853  ufileu  23862  fclscf  23968  flimfnfcls  23971  tsmsres  24087  trust  24173  restutopopn  24182  metustfbas  24501  restmetu  24514  xrtgioo  24751  xrsmopn  24757  clsocv  25207  cmetss  25273  ovoliunlem1  25460  difmbl  25501  voliunlem1  25508  volsup2  25563  i1fima  25636  i1fima2  25637  i1fd  25639  itg1addlem5  25658  itg1climres  25672  dvmptid  25918  dvmptc  25919  dvlipcn  25956  dvlip2  25957  dvcnvrelem1  25979  dvcvx  25982  taylthlem1  26338  taylthlem2  26339  taylthlem2OLD  26340  psercn  26393  pige3ALT  26486  dvlog  26617  dvcxp1  26706  ppiprm  27118  chtprm  27120  nolesgn2ores  27641  nogesgn1ores  27643  nodense  27661  nosupres  27676  nosupbnd2lem1  27684  noinfres  27691  noinfbnd2lem1  27699  lrrecpred  27908  onsiso  28226  bdayn0sf1o  28316  chm1i  31442  dmdsl3  32301  atssma  32364  dmdbr6ati  32409  imadifxp  32587  fnresin  32609  preimane  32653  fnpreimac  32654  mptprop  32680  df1stres  32686  df2ndres  32687  preiman0  32692  xrge0base  33011  xrge00  33012  gsumhashmul  33060  cycpm2tr  33135  xrge0slmod  33368  resssra  33632  fldexttr  33705  zarcmplem  33917  esumnul  34084  esumsnf  34100  baselcarsg  34343  difelcarsg  34347  eulerpartlemgs2  34417  probmeasb  34467  ballotlemfp1  34529  signstres  34612  ftc2re  34635  bnj1322  34858  cvmscld  35300  cvmliftmolem1  35308  mrsubvrs  35549  elmsta  35575  dfon2lem4  35809  dfrdg2  35818  fvline2  36169  topbnd  36347  opnbnd  36348  neibastop1  36382  bj-disj2r  37051  bj-restsnss2  37107  bj-0int  37124  bj-prmoore  37138  bj-inexeqex  37177  bj-idreseq  37185  mblfinlem3  37688  mblfinlem4  37689  ftc1anclem6  37727  areacirclem1  37737  subspopn  37781  ssbnd  37817  heiborlem3  37842  lcvexchlem3  39059  dihglblem5aN  41316  readvrec2  42379  readvcot  42382  elrfi  42692  setindtr  43023  fnwe2lem2  43050  lmhmlnmsplit  43086  proot1hash  43194  fgraphopab  43202  tfsconcatrev  43347  insucid  43402  iunrelexp0  43701  gneispace  44133  wfaxpow  44997  restsubel  45157  uzinico2  45570  limsupval3  45701  limsupvaluz  45717  liminfval5  45774  fouriersw  46240  saliinclf  46335  saldifcl2  46337  gsumge0cl  46380  sge0sn  46388  sge0tsms  46389  sge0split  46418  caragenunidm  46517  fnresfnco  47050  fcoreslem2  47073  3f1oss1  47084  imaelsetpreimafv  47389  resinsnALT  48828  iscnrm3rlem1  48894  iscnrm3rlem4  48897  incat  49458