Metamath Proof Explorer


Theorem unissb

Description: Relationship involving membership, subset, and union. Exercise 5 of Enderton p. 26 and its converse. (Contributed by NM, 20-Sep-2003) Avoid ax-11 . (Revised by BTernaryTau, 28-Dec-2024)

Ref Expression
Assertion unissb ABxAxB

Proof

Step Hyp Ref Expression
1 eluni yAxyxxA
2 1 imbi1i yAyBxyxxAyB
3 19.23v xyxxAyBxyxxAyB
4 2 3 bitr4i yAyBxyxxAyB
5 4 albii yyAyByxyxxAyB
6 elequ1 y=zyxzx
7 6 anbi1d y=zyxxAzxxA
8 eleq1w y=zyBzB
9 7 8 imbi12d y=zyxxAyBzxxAzB
10 elequ2 x=zyxyz
11 eleq1w x=zxAzA
12 10 11 anbi12d x=zyxxAyzzA
13 12 imbi1d x=zyxxAyByzzAyB
14 9 13 alcomw yxyxxAyBxyyxxAyB
15 19.21v yxAyxyBxAyyxyB
16 impexp yxxAyByxxAyB
17 bi2.04 yxxAyBxAyxyB
18 16 17 bitri yxxAyBxAyxyB
19 18 albii yyxxAyByxAyxyB
20 dfss2 xByyxyB
21 20 imbi2i xAxBxAyyxyB
22 15 19 21 3bitr4i yyxxAyBxAxB
23 22 albii xyyxxAyBxxAxB
24 14 23 bitri yxyxxAyBxxAxB
25 5 24 bitri yyAyBxxAxB
26 dfss2 AByyAyB
27 df-ral xAxBxxAxB
28 25 26 27 3bitr4i ABxAxB