Theorem dfss7 4182

Description: Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.)

Assertion

Ref	Expression
dfss7	⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss7

Step	Hyp	Ref	Expression
1		dfss2 3903	. 2 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐵)
2		dfin5 3893	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
3	2	ineqcomi 4143	. . 3 ⊢ (𝐵 ∩ 𝐴) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
4	3	eqeq1i 2746	. 2 ⊢ ((𝐵 ∩ 𝐴) = 𝐵 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵)
5	1, 4	bitri 277	1 ⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1548   ∈ wcel 2121  {crab 3393   ∩ cin 3884   ⊆ wss 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-in 3892  df-ss 3902

This theorem is referenced by:  qusker  33436  nsgqusf1olem3  33502  f1oresf1orab  47766