Theorem dfss2 4094

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3896. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3896. (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 4091	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2765	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3896	. . 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 2130	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 279	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 341	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1851	. . 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 1567   = wceq 1569  [wsb 2098   ∈ wcel 2144  {cab 2738   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-in 4091

This theorem is used by:  dfss  4095  sseqin2  4120  dfss7  4148  inabs  4211  nssinpss  4212  dfrab3ss  4268  disjssun  4420  riinn0  5042  ssexg  5280  ssexOLD  5282  op1stb  5439  ssdmres  6003  dmressnsn  6011  sspred  6313  ordtri3or  6395  fnimaeq0  6673  f0rn0  6768  fnreseql  7048  cnvimainrn  7067  sspreima  7068  sorpssin  7748  curry1  8118  curry2  8121  tpostpos2  8268  tz7.44-2  8419  tz7.44-3  8420  frfnom  8447  ecinxp  8817  infssuni  9339  elfiun  9426  marypha1lem  9429  unxpwdom  9587  djuinf  10271  ackbij1lem16  10316  fin23lem26  10407  isf34lem7  10461  isf34lem6  10462  fpwwe2lem10  10729  fpwwe2lem12  10731  fpwwe2  10732  uzin  13005  iooval2  13513  limsupgle  15650  limsupgre  15654  bitsinv1  16618  bitsres  16649  bitsuz  16650  2prm  16873  dfphi2  16957  ressbas2  17422  ressinbas  17429  ressval3d  17430  ressress  17431  restid2  17607  xrge0base  17785  resscatc  18290  symgvalstruct  19617  pmtrmvd  19676  dprdz  20252  dprdcntz2  20260  lmhmlsp  21330  lspdisj2  21411  lidlbas  21499  ressmplbas2  22341  psdmullem  22492  difopn  23358  mretopd  23416  restcld  23496  restopnb  23499  restfpw  23503  neitr  23504  cnrest2  23610  paste  23618  isnrm2  23682  1stccnp  23787  restnlly  23807  lly1stc  23821  kgeni  23862  kgencn3  23883  ptbasfi  23906  hausdiag  23970  qtopval2  24021  qtoprest  24042  trfil2  24212  trfg  24216  uzrest  24222  trufil  24235  ufileu  24244  fclscf  24350  flimfnfcls  24353  tsmsres  24469  trust  24554  restutopopn  24563  metustfbas  24882  restmetu  24895  xrtgioo  25132  xrsmopn  25138  clsocv  25577  cmetss  25643  ovoliunlem1  25829  difmbl  25870  voliunlem1  25877  volsup2  25932  i1fima  26005  i1fima2  26006  i1fd  26008  itg1addlem5  26027  itg1climres  26041  dvmptid  26283  dvmptc  26284  dvlipcn  26320  dvlip2  26321  dvcnvrelem1  26343  dvcvx  26346  taylthlem1  26706  taylthlem2  26707  psercn  26759  pige3ALT  26854  dvlog  26985  dvcxp1  27074  ppiprm  27484  chtprm  27486  nolesgn2ores  28035  nogesgn1ores  28037  nodense  28055  nosupres  28070  nosupbnd2lem1  28078  noinfres  28085  noinfbnd2lem1  28093  lrrecpred  28336  oniso  28663  bdayn0sf1o  28762  chm1i  32064  dmdsl3  32923  atssma  32986  dmdbr6ati  33031  imadifxp  33243  fnresin  33266  preimane  33311  fnpreimac  33312  mptprop  33339  df1stres  33345  df2ndres  33346  preiman0  33351  xrge00  33622  gsumhashmul  33675  cycpm2tr  33727  xrge0slmod  33956  psrbasfsupp  34190  resssra  34266  fldexttr  34337  zarcmplem  34560  esumnul  34727  esumsnf  34743  baselcarsg  34985  difelcarsg  34989  eulerpartlemgs2  35059  probmeasb  35109  ballotlemfp1  35171  signstres  35251  ftc2re  35274  bnj1322  35499  cvmscld  36125  cvmliftmolem1  36133  mrsubvrs  36374  elmsta  36400  dfon2lem4  36641  dfrdg2  36650  fvline2  37004  topbnd  37205  opnbnd  37206  neibastop1  37240  ttcwf2  37406  dfttc4  37411  bj-disj2r  38034  bj-restsnss2  38098  bj-0int  38115  bj-prmoore  38129  bj-inexeqex  38169  bj-idreseq  38177  mblfinlem3  38671  mblfinlem4  38672  ftc1anclem6  38710  areacirclem1  38720  subspopn  38780  ssbnd  38816  heiborlem3  38841  lcvexchlem3  40187  dihglblem5aN  42443  readvrec2  43506  readvcot  43509  elrfi  43799  setindtr  44125  lmhmlnmsplit  44183  proot1hash  44291  fgraphopab  44299  tfsconcatrev  44444  insucid  44499  iunrelexp0  44796  gneispace  45228  wfaxpow  46081  restsubel  46262  uzinico2  46667  limsupval3  46796  limsupvaluz  46812  liminfval5  46869  fouriersw  47335  saliinclf  47430  saldifcl2  47432  gsumge0cl  47475  sge0sn  47483  sge0tsms  47484  sge0split  47513  caragenunidm  47612  fnresfnco  48205  fcoreslem2  48228  3f1oss1  48239  imaelsetpreimafv  48571  resinsnALT  50080  iscnrm3rlem1  50148  iscnrm3rlem4  50151  incat  50833  parhomco2  50854  parhomco  50855  parcatid2  50857  parcatid  50858  parmapco2  50866  parmapco  50867