Theorem dfss2 3923

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3922. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3922. (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 3912	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2734	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3922	. . 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 3904   ⊆ wss 3905

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 3912  df-ss 3922

This theorem is referenced by:  dfss  3924  sseqin2  4176  dfss7  4204  inabs  4219  nssinpss  4220  dfrab3ss  4276  disjssun  4421  riinn0  5035  ssex  5263  op1stb  5418  ssdmres  5968  dmressnsn  5978  sspred  6262  ordtri3or  6343  fnimaeq0  6619  f0rn0  6713  fnreseql  6986  cnvimainrn  7005  sspreima  7006  sorpssin  7671  curry1  8044  curry2  8047  tpostpos2  8187  tz7.44-2  8336  tz7.44-3  8337  frfnom  8364  ecinxp  8726  infssuni  9255  elfiun  9339  marypha1lem  9342  unxpwdom  9500  djuinf  10102  ackbij1lem16  10147  fin23lem26  10238  isf34lem7  10292  isf34lem6  10293  fpwwe2lem10  10553  fpwwe2lem12  10555  fpwwe2  10556  uzin  12793  iooval2  13299  limsupgle  15402  limsupgre  15406  bitsinv1  16371  bitsres  16402  bitsuz  16403  2prm  16621  dfphi2  16703  ressbas2  17167  ressinbas  17174  ressval3d  17175  ressress  17176  restid2  17352  xrge0base  17529  resscatc  18034  symgvalstruct  19294  pmtrmvd  19353  dprdz  19929  dprdcntz2  19937  lmhmlsp  20971  lspdisj2  21052  lidlbas  21139  ressmplbas2  21950  psdmullem  22068  difopn  22937  mretopd  22995  restcld  23075  restopnb  23078  restfpw  23082  neitr  23083  cnrest2  23189  paste  23197  isnrm2  23261  1stccnp  23365  restnlly  23385  lly1stc  23399  kgeni  23440  kgencn3  23461  ptbasfi  23484  hausdiag  23548  qtopval2  23599  qtoprest  23620  trfil2  23790  trfg  23794  uzrest  23800  trufil  23813  ufileu  23822  fclscf  23928  flimfnfcls  23931  tsmsres  24047  trust  24133  restutopopn  24142  metustfbas  24461  restmetu  24474  xrtgioo  24711  xrsmopn  24717  clsocv  25166  cmetss  25232  ovoliunlem1  25419  difmbl  25460  voliunlem1  25467  volsup2  25522  i1fima  25595  i1fima2  25596  i1fd  25598  itg1addlem5  25617  itg1climres  25631  dvmptid  25877  dvmptc  25878  dvlipcn  25915  dvlip2  25916  dvcnvrelem1  25938  dvcvx  25941  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  psercn  26352  pige3ALT  26445  dvlog  26576  dvcxp1  26665  ppiprm  27077  chtprm  27079  nolesgn2ores  27600  nogesgn1ores  27602  nodense  27620  nosupres  27635  nosupbnd2lem1  27643  noinfres  27650  noinfbnd2lem1  27658  lrrecpred  27874  onsiso  28192  bdayn0sf1o  28282  chm1i  31418  dmdsl3  32277  atssma  32340  dmdbr6ati  32385  imadifxp  32563  fnresin  32583  preimane  32627  fnpreimac  32628  mptprop  32654  df1stres  32660  df2ndres  32661  preiman0  32666  xrge00  32981  gsumhashmul  33027  cycpm2tr  33074  xrge0slmod  33298  resssra  33562  fldexttr  33633  zarcmplem  33850  esumnul  34017  esumsnf  34033  baselcarsg  34276  difelcarsg  34280  eulerpartlemgs2  34350  probmeasb  34400  ballotlemfp1  34462  signstres  34545  ftc2re  34568  bnj1322  34791  cvmscld  35248  cvmliftmolem1  35256  mrsubvrs  35497  elmsta  35523  dfon2lem4  35762  dfrdg2  35771  fvline2  36122  topbnd  36300  opnbnd  36301  neibastop1  36335  bj-disj2r  37004  bj-restsnss2  37060  bj-0int  37077  bj-prmoore  37091  bj-inexeqex  37130  bj-idreseq  37138  mblfinlem3  37641  mblfinlem4  37642  ftc1anclem6  37680  areacirclem1  37690  subspopn  37734  ssbnd  37770  heiborlem3  37795  lcvexchlem3  39017  dihglblem5aN  41274  readvrec2  42337  readvcot  42340  elrfi  42670  setindtr  43000  fnwe2lem2  43027  lmhmlnmsplit  43063  proot1hash  43171  fgraphopab  43179  tfsconcatrev  43324  insucid  43379  iunrelexp0  43678  gneispace  44110  wfaxpow  44974  restsubel  45134  uzinico2  45546  limsupval3  45677  limsupvaluz  45693  liminfval5  45750  fouriersw  46216  saliinclf  46311  saldifcl2  46313  gsumge0cl  46356  sge0sn  46364  sge0tsms  46365  sge0split  46394  caragenunidm  46493  fnresfnco  47029  fcoreslem2  47052  3f1oss1  47063  imaelsetpreimafv  47383  resinsnALT  48861  iscnrm3rlem1  48928  iscnrm3rlem4  48931  incat  49590