Theorem dfss2 3907

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  [wsb 2068   ∈ wcel 2114  {cab 2714   ∩ cin 3888   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-in 3896  df-ss 3906

This theorem is referenced by:  dfss  3908  sseqin2  4163  dfss7  4191  inabs  4206  nssinpss  4207  dfrab3ss  4263  disjssun  4408  riinn0  5025  ssex  5262  op1stb  5424  ssdmres  5978  dmressnsn  5988  sspred  6274  ordtri3or  6355  fnimaeq0  6631  f0rn0  6725  fnreseql  7000  cnvimainrn  7019  sspreima  7020  sorpssin  7685  curry1  8054  curry2  8057  tpostpos2  8197  tz7.44-2  8346  tz7.44-3  8347  frfnom  8374  ecinxp  8739  infssuni  9256  elfiun  9343  marypha1lem  9346  unxpwdom  9504  djuinf  10111  ackbij1lem16  10156  fin23lem26  10247  isf34lem7  10301  isf34lem6  10302  fpwwe2lem10  10563  fpwwe2lem12  10565  fpwwe2  10566  uzin  12824  iooval2  13331  limsupgle  15439  limsupgre  15443  bitsinv1  16411  bitsres  16442  bitsuz  16443  2prm  16661  dfphi2  16744  ressbas2  17208  ressinbas  17215  ressval3d  17216  ressress  17217  restid2  17393  xrge0base  17571  resscatc  18076  symgvalstruct  19372  pmtrmvd  19431  dprdz  20007  dprdcntz2  20015  lmhmlsp  21044  lspdisj2  21125  lidlbas  21212  ressmplbas2  22005  psdmullem  22131  difopn  22999  mretopd  23057  restcld  23137  restopnb  23140  restfpw  23144  neitr  23145  cnrest2  23251  paste  23259  isnrm2  23323  1stccnp  23427  restnlly  23447  lly1stc  23461  kgeni  23502  kgencn3  23523  ptbasfi  23546  hausdiag  23610  qtopval2  23661  qtoprest  23682  trfil2  23852  trfg  23856  uzrest  23862  trufil  23875  ufileu  23884  fclscf  23990  flimfnfcls  23993  tsmsres  24109  trust  24194  restutopopn  24203  metustfbas  24522  restmetu  24535  xrtgioo  24772  xrsmopn  24778  clsocv  25217  cmetss  25283  ovoliunlem1  25469  difmbl  25510  voliunlem1  25517  volsup2  25572  i1fima  25645  i1fima2  25646  i1fd  25648  itg1addlem5  25667  itg1climres  25681  dvmptid  25924  dvmptc  25925  dvlipcn  25961  dvlip2  25962  dvcnvrelem1  25984  dvcvx  25987  taylthlem1  26338  taylthlem2  26339  psercn  26391  pige3ALT  26484  dvlog  26615  dvcxp1  26704  ppiprm  27114  chtprm  27116  nolesgn2ores  27636  nogesgn1ores  27638  nodense  27656  nosupres  27671  nosupbnd2lem1  27679  noinfres  27686  noinfbnd2lem1  27694  lrrecpred  27936  oniso  28263  bdayn0sf1o  28362  chm1i  31527  dmdsl3  32386  atssma  32449  dmdbr6ati  32494  imadifxp  32671  fnresin  32697  preimane  32742  fnpreimac  32743  mptprop  32771  df1stres  32777  df2ndres  32778  preiman0  32783  xrge00  33074  gsumhashmul  33128  cycpm2tr  33180  xrge0slmod  33408  psrbasfsupp  33672  resssra  33731  fldexttr  33802  zarcmplem  34025  esumnul  34192  esumsnf  34208  baselcarsg  34450  difelcarsg  34454  eulerpartlemgs2  34524  probmeasb  34574  ballotlemfp1  34636  signstres  34719  ftc2re  34742  bnj1322  34964  cvmscld  35455  cvmliftmolem1  35463  mrsubvrs  35704  elmsta  35730  dfon2lem4  35966  dfrdg2  35975  fvline2  36328  topbnd  36506  opnbnd  36507  neibastop1  36541  ttcwf2  36707  dfttc4  36712  bj-disj2r  37335  bj-restsnss2  37396  bj-0int  37413  bj-prmoore  37427  bj-inexeqex  37468  bj-idreseq  37476  mblfinlem3  37980  mblfinlem4  37981  ftc1anclem6  38019  areacirclem1  38029  subspopn  38073  ssbnd  38109  heiborlem3  38134  lcvexchlem3  39482  dihglblem5aN  41738  readvrec2  42793  readvcot  42796  elrfi  43126  setindtr  43452  fnwe2lem2  43479  lmhmlnmsplit  43515  proot1hash  43623  fgraphopab  43631  tfsconcatrev  43776  insucid  43831  iunrelexp0  44129  gneispace  44561  wfaxpow  45424  restsubel  45583  uzinico2  45991  limsupval3  46120  limsupvaluz  46136  liminfval5  46193  fouriersw  46659  saliinclf  46754  saldifcl2  46756  gsumge0cl  46799  sge0sn  46807  sge0tsms  46808  sge0split  46837  caragenunidm  46936  fnresfnco  47489  fcoreslem2  47512  3f1oss1  47523  imaelsetpreimafv  47855  resinsnALT  49348  iscnrm3rlem1  49415  iscnrm3rlem4  49418  incat  50076