Theorem dfss2 3951

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537   = wceq 1539  [wsb 2063   ∈ wcel 2107  {cab 2712   ∩ cin 3932   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-in 3940  df-ss 3950

This theorem is referenced by:  dfss  3952  sseqin2  4205  dfss7  4233  inabs  4248  nssinpss  4249  dfrab3ss  4305  disjssun  4450  riinn0  5065  ssex  5303  op1stb  5458  ssdmres  6013  dmressnsn  6023  sspred  6312  ordtri3or  6397  fnimaeq0  6682  f0rn0  6774  fnreseql  7049  cnvimainrn  7068  sspreima  7069  sorpssin  7734  curry1  8112  curry2  8115  tpostpos2  8255  tz7.44-2  8430  tz7.44-3  8431  frfnom  8458  ecinxp  8815  infssuni  9369  elfiun  9453  marypha1lem  9456  unxpwdom  9612  djuinf  10212  ackbij1lem16  10257  fin23lem26  10348  isf34lem7  10402  isf34lem6  10403  fpwwe2lem10  10663  fpwwe2lem12  10665  fpwwe2  10666  uzin  12901  iooval2  13403  limsupgle  15496  limsupgre  15500  bitsinv1  16462  bitsres  16493  bitsuz  16494  2prm  16712  dfphi2  16794  ressbas2  17265  ressinbas  17272  ressval3d  17273  ressress  17274  restid2  17451  resscatc  18130  symgvalstruct  19387  symgvalstructOLD  19388  pmtrmvd  19447  dprdz  20023  dprdcntz2  20031  lmhmlsp  21021  lspdisj2  21102  lidlbas  21191  ressmplbas2  22012  psdmullem  22136  difopn  23007  mretopd  23065  restcld  23145  restopnb  23148  restfpw  23152  neitr  23153  cnrest2  23259  paste  23267  isnrm2  23331  1stccnp  23435  restnlly  23455  lly1stc  23469  kgeni  23510  kgencn3  23531  ptbasfi  23554  hausdiag  23618  qtopval2  23669  qtoprest  23690  trfil2  23860  trfg  23864  uzrest  23870  trufil  23883  ufileu  23892  fclscf  23998  flimfnfcls  24001  tsmsres  24117  trust  24203  restutopopn  24212  metustfbas  24533  restmetu  24546  xrtgioo  24783  xrsmopn  24789  clsocv  25239  cmetss  25305  ovoliunlem1  25492  difmbl  25533  voliunlem1  25540  volsup2  25595  i1fima  25668  i1fima2  25669  i1fd  25671  itg1addlem5  25690  itg1climres  25704  dvmptid  25950  dvmptc  25951  dvlipcn  25988  dvlip2  25989  dvcnvrelem1  26011  dvcvx  26014  taylthlem1  26370  taylthlem2  26371  taylthlem2OLD  26372  psercn  26425  pige3ALT  26517  dvlog  26648  dvcxp1  26737  ppiprm  27149  chtprm  27151  nolesgn2ores  27672  nogesgn1ores  27674  nodense  27692  nosupres  27707  nosupbnd2lem1  27715  noinfres  27722  noinfbnd2lem1  27730  lrrecpred  27932  chm1i  31422  dmdsl3  32281  atssma  32344  dmdbr6ati  32389  imadifxp  32561  fnresin  32583  preimane  32627  fnpreimac  32628  mptprop  32654  df1stres  32660  df2ndres  32661  preiman0  32666  xrge0base  32962  xrge00  32963  gsumhashmul  33010  cycpm2tr  33085  xrge0slmod  33317  resssra  33579  fldexttr  33650  zarcmplem  33821  esumnul  33990  esumsnf  34006  baselcarsg  34249  difelcarsg  34253  eulerpartlemgs2  34323  probmeasb  34373  ballotlemfp1  34435  signstres  34531  ftc2re  34554  bnj1322  34777  cvmscld  35219  cvmliftmolem1  35227  mrsubvrs  35468  elmsta  35494  dfon2lem4  35728  dfrdg2  35737  fvline2  36088  topbnd  36266  opnbnd  36267  neibastop1  36301  bj-disj2r  36970  bj-restsnss2  37026  bj-0int  37043  bj-prmoore  37057  bj-inexeqex  37096  bj-idreseq  37104  mblfinlem3  37607  mblfinlem4  37608  ftc1anclem6  37646  areacirclem1  37656  subspopn  37700  ssbnd  37736  heiborlem3  37761  lcvexchlem3  38978  dihglblem5aN  41235  readvrec2  42336  readvcot  42339  elrfi  42650  setindtr  42981  fnwe2lem2  43008  lmhmlnmsplit  43044  proot1hash  43152  fgraphopab  43160  tfsconcatrev  43306  insucid  43361  iunrelexp0  43660  gneispace  44092  wfaxpow  44959  restsubel  45103  uzinico2  45520  limsupval3  45652  limsupvaluz  45668  liminfval5  45725  fouriersw  46191  saliinclf  46286  saldifcl2  46288  gsumge0cl  46331  sge0sn  46339  sge0tsms  46340  sge0split  46369  caragenunidm  46468  fnresfnco  46999  fcoreslem2  47022  3f1oss1  47033  imaelsetpreimafv  47328  resinsnALT  48720  iscnrm3rlem1  48785  iscnrm3rlem4  48788