Theorem dfss2 3916

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  [wsb 2067   ∈ wcel 2113  {cab 2711   ∩ cin 3897   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-in 3905  df-ss 3915

This theorem is referenced by:  dfss  3917  sseqin2  4172  dfss7  4200  inabs  4215  nssinpss  4216  dfrab3ss  4272  disjssun  4417  riinn0  5035  ssex  5263  op1stb  5416  ssdmres  5968  dmressnsn  5978  sspred  6264  ordtri3or  6345  fnimaeq0  6621  f0rn0  6715  fnreseql  6989  cnvimainrn  7008  sspreima  7009  sorpssin  7672  curry1  8042  curry2  8045  tpostpos2  8185  tz7.44-2  8334  tz7.44-3  8335  frfnom  8362  ecinxp  8724  infssuni  9239  elfiun  9323  marypha1lem  9326  unxpwdom  9484  djuinf  10089  ackbij1lem16  10134  fin23lem26  10225  isf34lem7  10279  isf34lem6  10280  fpwwe2lem10  10540  fpwwe2lem12  10542  fpwwe2  10543  uzin  12776  iooval2  13282  limsupgle  15388  limsupgre  15392  bitsinv1  16357  bitsres  16388  bitsuz  16389  2prm  16607  dfphi2  16689  ressbas2  17153  ressinbas  17160  ressval3d  17161  ressress  17162  restid2  17338  xrge0base  17515  resscatc  18020  symgvalstruct  19313  pmtrmvd  19372  dprdz  19948  dprdcntz2  19956  lmhmlsp  20987  lspdisj2  21068  lidlbas  21155  ressmplbas2  21965  psdmullem  22083  difopn  22952  mretopd  23010  restcld  23090  restopnb  23093  restfpw  23097  neitr  23098  cnrest2  23204  paste  23212  isnrm2  23276  1stccnp  23380  restnlly  23400  lly1stc  23414  kgeni  23455  kgencn3  23476  ptbasfi  23499  hausdiag  23563  qtopval2  23614  qtoprest  23635  trfil2  23805  trfg  23809  uzrest  23815  trufil  23828  ufileu  23837  fclscf  23943  flimfnfcls  23946  tsmsres  24062  trust  24147  restutopopn  24156  metustfbas  24475  restmetu  24488  xrtgioo  24725  xrsmopn  24731  clsocv  25180  cmetss  25246  ovoliunlem1  25433  difmbl  25474  voliunlem1  25481  volsup2  25536  i1fima  25609  i1fima2  25610  i1fd  25612  itg1addlem5  25631  itg1climres  25645  dvmptid  25891  dvmptc  25892  dvlipcn  25929  dvlip2  25930  dvcnvrelem1  25952  dvcvx  25955  taylthlem1  26311  taylthlem2  26312  taylthlem2OLD  26313  psercn  26366  pige3ALT  26459  dvlog  26590  dvcxp1  26679  ppiprm  27091  chtprm  27093  nolesgn2ores  27614  nogesgn1ores  27616  nodense  27634  nosupres  27649  nosupbnd2lem1  27657  noinfres  27664  noinfbnd2lem1  27672  lrrecpred  27890  onsiso  28208  bdayn0sf1o  28298  chm1i  31440  dmdsl3  32299  atssma  32362  dmdbr6ati  32407  imadifxp  32585  fnresin  32611  preimane  32656  fnpreimac  32657  mptprop  32685  df1stres  32691  df2ndres  32692  preiman0  32697  xrge00  33004  gsumhashmul  33050  cycpm2tr  33097  xrge0slmod  33322  psrbasfsupp  33581  resssra  33622  fldexttr  33694  zarcmplem  33917  esumnul  34084  esumsnf  34100  baselcarsg  34342  difelcarsg  34346  eulerpartlemgs2  34416  probmeasb  34466  ballotlemfp1  34528  signstres  34611  ftc2re  34634  bnj1322  34857  cvmscld  35340  cvmliftmolem1  35348  mrsubvrs  35589  elmsta  35615  dfon2lem4  35851  dfrdg2  35860  fvline2  36213  topbnd  36391  opnbnd  36392  neibastop1  36426  bj-disj2r  37095  bj-restsnss2  37151  bj-0int  37168  bj-prmoore  37182  bj-inexeqex  37221  bj-idreseq  37229  mblfinlem3  37722  mblfinlem4  37723  ftc1anclem6  37761  areacirclem1  37771  subspopn  37815  ssbnd  37851  heiborlem3  37876  lcvexchlem3  39158  dihglblem5aN  41414  readvrec2  42482  readvcot  42485  elrfi  42814  setindtr  43144  fnwe2lem2  43171  lmhmlnmsplit  43207  proot1hash  43315  fgraphopab  43323  tfsconcatrev  43468  insucid  43523  iunrelexp0  43822  gneispace  44254  wfaxpow  45117  restsubel  45277  uzinico2  45688  limsupval3  45817  limsupvaluz  45833  liminfval5  45890  fouriersw  46356  saliinclf  46451  saldifcl2  46453  gsumge0cl  46496  sge0sn  46504  sge0tsms  46505  sge0split  46534  caragenunidm  46633  fnresfnco  47168  fcoreslem2  47191  3f1oss1  47202  imaelsetpreimafv  47522  resinsnALT  49000  iscnrm3rlem1  49067  iscnrm3rlem4  49070  incat  49729