Theorem dfss2 3924

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3923. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3923. (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 2756	. 2 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
2		df-in 3913	. . 3 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3	2	eqeq1i 2768	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = 𝐴)
4		df-ss 3923	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5		simp2 1155	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
6	5	3expib 1140	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴))
7		ancl 553	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	6, 7	impbid 215	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
9		dfbi2 479	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))))
10		pm2.21 124	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
11		pm3.4 821	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
12	10, 11	ja 188	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
13	9, 12	simplbiim 513	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
14	8, 13	impbii 212	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴))
15		df-clab 2742	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ [𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
16		eleq1w 2846	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17		eleq1w 2846	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
18	16, 17	anbi12d 643	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
19	18	sbievw 2128	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	15, 19	bitr2i 279	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21	20	bibi1i 341	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
22	14, 21	bitri 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
23	22	albii 1849	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
24	4, 23	bitri 278	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} ↔ 𝑥 ∈ 𝐴))
25	1, 3, 24	3bitr4ri 307	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570  [wsb 2096   ∈ wcel 2143  {cab 2741   ∩ cin 3905   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-in 3913  df-ss 3923

This theorem is referenced by:  dfss  3925  sseqin2  4177  dfss7  4205  inabs  4220  nssinpss  4221  dfrab3ss  4277  disjssun  4429  riinn0  5050  ssexg  5291  ssexOLD  5293  op1stb  5455  ssdmres  6014  dmressnsn  6024  sspred  6313  ordtri3or  6395  fnimaeq0  6670  f0rn0  6765  fnreseql  7045  cnvimainrn  7064  sspreima  7065  sorpssin  7730  curry1  8100  curry2  8103  tpostpos2  8244  tz7.44-2  8395  tz7.44-3  8396  frfnom  8423  ecinxp  8791  infssuni  9304  elfiun  9391  marypha1lem  9394  unxpwdom  9552  djuinf  10173  ackbij1lem16  10218  fin23lem26  10310  isf34lem7  10364  isf34lem6  10365  fpwwe2lem10  10626  fpwwe2lem12  10628  fpwwe2  10629  uzin  12899  iooval2  13406  limsupgle  15530  limsupgre  15534  bitsinv1  16501  bitsres  16532  bitsuz  16533  2prm  16751  dfphi2  16834  ressbas2  17299  ressinbas  17306  ressval3d  17307  ressress  17308  restid2  17484  xrge0base  17662  resscatc  18167  symgvalstruct  19468  pmtrmvd  19527  dprdz  20103  dprdcntz2  20111  lmhmlsp  21151  lspdisj2  21232  lidlbas  21320  ressmplbas2  22158  psdmullem  22309  difopn  23172  mretopd  23230  restcld  23310  restopnb  23313  restfpw  23317  neitr  23318  cnrest2  23424  paste  23432  isnrm2  23496  1stccnp  23600  restnlly  23620  lly1stc  23634  kgeni  23675  kgencn3  23696  ptbasfi  23719  hausdiag  23783  qtopval2  23834  qtoprest  23855  trfil2  24025  trfg  24029  uzrest  24035  trufil  24048  ufileu  24057  fclscf  24163  flimfnfcls  24166  tsmsres  24282  trust  24367  restutopopn  24376  metustfbas  24695  restmetu  24708  xrtgioo  24945  xrsmopn  24951  clsocv  25390  cmetss  25456  ovoliunlem1  25642  difmbl  25683  voliunlem1  25690  volsup2  25745  i1fima  25818  i1fima2  25819  i1fd  25821  itg1addlem5  25840  itg1climres  25854  dvmptid  26097  dvmptc  26098  dvlipcn  26134  dvlip2  26135  dvcnvrelem1  26157  dvcvx  26160  taylthlem1  26517  taylthlem2  26518  psercn  26570  pige3ALT  26666  dvlog  26797  dvcxp1  26886  ppiprm  27296  chtprm  27298  nolesgn2ores  27817  nogesgn1ores  27819  nodense  27837  nosupres  27852  nosupbnd2lem1  27860  noinfres  27867  noinfbnd2lem1  27875  lrrecpred  28118  oniso  28445  bdayn0sf1o  28544  chm1i  31789  dmdsl3  32648  atssma  32711  dmdbr6ati  32756  imadifxp  32927  fnresin  32950  preimane  32995  fnpreimac  32996  mptprop  33024  df1stres  33030  df2ndres  33031  preiman0  33036  xrge00  33315  gsumhashmul  33368  cycpm2tr  33420  xrge0slmod  33649  psrbasfsupp  33882  resssra  33958  fldexttr  34029  zarcmplem  34252  esumnul  34419  esumsnf  34435  baselcarsg  34677  difelcarsg  34681  eulerpartlemgs2  34751  probmeasb  34801  ballotlemfp1  34863  signstres  34943  ftc2re  34966  bnj1322  35191  cvmscld  35746  cvmliftmolem1  35754  mrsubvrs  35995  elmsta  36021  dfon2lem4  36257  dfrdg2  36266  fvline2  36619  topbnd  36816  opnbnd  36817  neibastop1  36851  ttcwf2  37017  dfttc4  37022  bj-disj2r  37645  bj-restsnss2  37707  bj-0int  37724  bj-prmoore  37738  bj-inexeqex  37779  bj-idreseq  37787  mblfinlem3  38291  mblfinlem4  38292  ftc1anclem6  38330  areacirclem1  38340  subspopn  38384  ssbnd  38420  heiborlem3  38445  lcvexchlem3  39791  dihglblem5aN  42047  readvrec2  43103  readvcot  43106  elrfi  43408  setindtr  43734  fnwe2lem2  43761  lmhmlnmsplit  43797  proot1hash  43905  fgraphopab  43913  tfsconcatrev  44058  insucid  44113  iunrelexp0  44411  gneispace  44843  wfaxpow  45689  restsubel  45854  uzinico2  46260  limsupval3  46389  limsupvaluz  46405  liminfval5  46462  fouriersw  46928  saliinclf  47023  saldifcl2  47025  gsumge0cl  47068  sge0sn  47076  sge0tsms  47077  sge0split  47106  caragenunidm  47205  fnresfnco  47761  fcoreslem2  47784  3f1oss1  47795  imaelsetpreimafv  48127  resinsnALT  49634  iscnrm3rlem1  49701  iscnrm3rlem4  49704  incat  50362