Metamath Proof Explorer

Theorem brsset

Description: For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Hypothesis brsset.1 ⊒B∈V
Assertion brsset ⊒A𝖲𝖲𝖾𝗍B↔AβŠ†B

Proof

Step Hyp Ref Expression
1 brsset.1 ⊒B∈V
2 relsset ⊒Rel⁑𝖲𝖲𝖾𝗍
3 2 brrelex1i ⊒A𝖲𝖲𝖾𝗍Bβ†’A∈V
4 1 ssex ⊒AβŠ†Bβ†’A∈V
5 breq1 ⊒x=Aβ†’x𝖲𝖲𝖾𝗍B↔A𝖲𝖲𝖾𝗍B
6 sseq1 ⊒x=Aβ†’xβŠ†B↔AβŠ†B
7 opex ⊒xB∈V
8 7 elrn ⊒xB∈ran⁑EβŠ—Vβˆ–Eβ†”βˆƒyyEβŠ—Vβˆ–ExB
9 vex ⊒y∈V
10 vex ⊒x∈V
11 9 10 1 brtxp ⊒yEβŠ—Vβˆ–ExB↔yEx∧yVβˆ–EB
12 epel ⊒yEx↔y∈x
13 brv ⊒yVB
14 brdif ⊒yVβˆ–EB↔yVB∧¬yEB
15 13 14 mpbiran ⊒yVβˆ–EB↔¬yEB
16 1 epeli ⊒yEB↔y∈B
17 15 16 xchbinx ⊒yVβˆ–EB↔¬y∈B
18 12 17 anbi12i ⊒yEx∧yVβˆ–EB↔y∈x∧¬y∈B
19 11 18 bitri ⊒yEβŠ—Vβˆ–ExB↔y∈x∧¬y∈B
20 19 exbii βŠ’βˆƒyyEβŠ—Vβˆ–ExBβ†”βˆƒyy∈x∧¬y∈B
21 exanali βŠ’βˆƒyy∈x∧¬y∈Bβ†”Β¬βˆ€yy∈xβ†’y∈B
22 8 20 21 3bitrri βŠ’Β¬βˆ€yy∈xβ†’y∈B↔xB∈ran⁑EβŠ—Vβˆ–E
23 22 con1bii ⊒¬xB∈ran⁑EβŠ—Vβˆ–Eβ†”βˆ€yy∈xβ†’y∈B
24 df-br ⊒x𝖲𝖲𝖾𝗍B↔xBβˆˆπ–²π–²π–Ύπ—
25 df-sset βŠ’π–²π–²π–Ύπ—=VΓ—Vβˆ–ran⁑EβŠ—Vβˆ–E
26 25 eleq2i ⊒xBβˆˆπ–²π–²π–Ύπ—β†”xB∈VΓ—Vβˆ–ran⁑EβŠ—Vβˆ–E
27 10 1 opelvv ⊒xB∈VΓ—V
28 eldif ⊒xB∈VΓ—Vβˆ–ran⁑EβŠ—Vβˆ–E↔xB∈VΓ—V∧¬xB∈ran⁑EβŠ—Vβˆ–E
29 27 28 mpbiran ⊒xB∈VΓ—Vβˆ–ran⁑EβŠ—Vβˆ–E↔¬xB∈ran⁑EβŠ—Vβˆ–E
30 26 29 bitri ⊒xBβˆˆπ–²π–²π–Ύπ—β†”Β¬xB∈ran⁑EβŠ—Vβˆ–E
31 24 30 bitri ⊒x𝖲𝖲𝖾𝗍B↔¬xB∈ran⁑EβŠ—Vβˆ–E
32 dfss2 ⊒xβŠ†Bβ†”βˆ€yy∈xβ†’y∈B
33 23 31 32 3bitr4i ⊒x𝖲𝖲𝖾𝗍B↔xβŠ†B
34 5 6 33 vtoclbg ⊒A∈Vβ†’A𝖲𝖲𝖾𝗍B↔AβŠ†B
35 3 4 34 pm5.21nii ⊒A𝖲𝖲𝖾𝗍B↔AβŠ†B