Theorem dfss2 3917

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3916. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3916. (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 2753	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3906	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2765	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3916	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1155	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1140	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴))
7		ancl 554	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	6, 7	impbid 215	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
9		dfbi2 480	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))))
10		pm2.21 124	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
11		pm3.4 822	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
12	10, 11	ja 188	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
13	9, 12	simplbiim 514	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
14	8, 13	impbii 212	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
15		df-clab 2739	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2843	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2843	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 644	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2131	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 279	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 341	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 278	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 307	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  [wsb 2099   ∈ wcel 2145  {cab 2738   ∩ cin 3898   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-in 3906  df-ss 3916

This theorem is used by:  dfss  3918  sseqin2  4169  dfss7  4197  inabs  4212  nssinpss  4213  dfrab3ss  4269  disjssun  4421  riinn0  5043  ssexg  5284  ssexOLD  5286  op1stb  5447  ssdmres  6006  dmressnsn  6016  sspred  6308  ordtri3or  6390  fnimaeq0  6665  f0rn0  6760  fnreseql  7040  cnvimainrn  7059  sspreima  7060  sorpssin  7732  curry1  8101  curry2  8104  tpostpos2  8245  tz7.44-2  8396  tz7.44-3  8397  frfnom  8424  ecinxp  8792  infssuni  9313  elfiun  9400  marypha1lem  9403  unxpwdom  9561  djuinf  10191  ackbij1lem16  10236  fin23lem26  10327  isf34lem7  10381  isf34lem6  10382  fpwwe2lem10  10649  fpwwe2lem12  10651  fpwwe2  10652  uzin  12923  iooval2  13431  limsupgle  15564  limsupgre  15568  bitsinv1  16532  bitsres  16563  bitsuz  16564  2prm  16782  dfphi2  16865  ressbas2  17330  ressinbas  17337  ressval3d  17338  ressress  17339  restid2  17515  xrge0base  17693  resscatc  18198  symgvalstruct  19524  pmtrmvd  19583  dprdz  20159  dprdcntz2  20167  lmhmlsp  21233  lspdisj2  21314  lidlbas  21402  ressmplbas2  22242  psdmullem  22393  difopn  23259  mretopd  23317  restcld  23397  restopnb  23400  restfpw  23404  neitr  23405  cnrest2  23511  paste  23519  isnrm2  23583  1stccnp  23688  restnlly  23708  lly1stc  23722  kgeni  23763  kgencn3  23784  ptbasfi  23807  hausdiag  23871  qtopval2  23922  qtoprest  23943  trfil2  24113  trfg  24117  uzrest  24123  trufil  24136  ufileu  24145  fclscf  24251  flimfnfcls  24254  tsmsres  24370  trust  24455  restutopopn  24464  metustfbas  24783  restmetu  24796  xrtgioo  25033  xrsmopn  25039  clsocv  25478  cmetss  25544  ovoliunlem1  25730  difmbl  25771  voliunlem1  25778  volsup2  25833  i1fima  25906  i1fima2  25907  i1fd  25909  itg1addlem5  25928  itg1climres  25942  dvmptid  26184  dvmptc  26185  dvlipcn  26221  dvlip2  26222  dvcnvrelem1  26244  dvcvx  26247  taylthlem1  26609  taylthlem2  26610  psercn  26662  pige3ALT  26757  dvlog  26888  dvcxp1  26977  ppiprm  27387  chtprm  27389  nolesgn2ores  27908  nogesgn1ores  27910  nodense  27928  nosupres  27943  nosupbnd2lem1  27951  noinfres  27958  noinfbnd2lem1  27966  lrrecpred  28209  oniso  28536  bdayn0sf1o  28635  chm1i  31937  dmdsl3  32796  atssma  32859  dmdbr6ati  32904  imadifxp  33074  fnresin  33097  preimane  33142  fnpreimac  33143  mptprop  33170  df1stres  33176  df2ndres  33177  preiman0  33182  xrge00  33454  gsumhashmul  33507  cycpm2tr  33559  xrge0slmod  33788  psrbasfsupp  34021  resssra  34097  fldexttr  34168  zarcmplem  34391  esumnul  34558  esumsnf  34574  baselcarsg  34817  difelcarsg  34821  eulerpartlemgs2  34891  probmeasb  34941  ballotlemfp1  35003  signstres  35083  ftc2re  35106  bnj1322  35331  cvmscld  35852  cvmliftmolem1  35860  mrsubvrs  36101  elmsta  36127  dfon2lem4  36363  dfrdg2  36372  fvline2  36726  topbnd  36943  opnbnd  36944  neibastop1  36978  ttcwf2  37144  dfttc4  37149  bj-disj2r  37772  bj-restsnss2  37834  bj-0int  37851  bj-prmoore  37865  bj-inexeqex  37906  bj-idreseq  37914  mblfinlem3  38408  mblfinlem4  38409  ftc1anclem6  38447  areacirclem1  38457  subspopn  38502  ssbnd  38538  heiborlem3  38563  lcvexchlem3  39909  dihglblem5aN  42165  readvrec2  43236  readvcot  43239  elrfi  43539  setindtr  43865  fnwe2lem2  43892  lmhmlnmsplit  43928  proot1hash  44036  fgraphopab  44044  tfsconcatrev  44189  insucid  44244  iunrelexp0  44542  gneispace  44974  wfaxpow  45820  restsubel  45985  uzinico2  46391  limsupval3  46520  limsupvaluz  46536  liminfval5  46593  fouriersw  47059  saliinclf  47154  saldifcl2  47156  gsumge0cl  47199  sge0sn  47207  sge0tsms  47208  sge0split  47237  caragenunidm  47336  fnresfnco  47929  fcoreslem2  47952  3f1oss1  47963  imaelsetpreimafv  48295  resinsnALT  49799  iscnrm3rlem1  49866  iscnrm3rlem4  49869  incat  50527