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 A B x A x B

Proof

Step Hyp Ref Expression
1 eluni y A x y x x A
2 1 imbi1i y A y B x y x x A y B
3 19.23v x y x x A y B x y x x A y B
4 2 3 bitr4i y A y B x y x x A y B
5 4 albii y y A y B y x y x x A y B
6 elequ1 y = z y x z x
7 6 anbi1d y = z y x x A z x x A
8 eleq1w y = z y B z B
9 7 8 imbi12d y = z y x x A y B z x x A z B
10 elequ2 x = z y x y z
11 eleq1w x = z x A z A
12 10 11 anbi12d x = z y x x A y z z A
13 12 imbi1d x = z y x x A y B y z z A y B
14 9 13 alcomw y x y x x A y B x y y x x A y B
15 19.21v y x A y x y B x A y y x y B
16 impexp y x x A y B y x x A y B
17 bi2.04 y x x A y B x A y x y B
18 16 17 bitri y x x A y B x A y x y B
19 18 albii y y x x A y B y x A y x y B
20 dfss2 x B y y x y B
21 20 imbi2i x A x B x A y y x y B
22 15 19 21 3bitr4i y y x x A y B x A x B
23 22 albii x y y x x A y B x x A x B
24 14 23 bitri y x y x x A y B x x A x B
25 5 24 bitri y y A y B x x A x B
26 dfss2 A B y y A y B
27 df-ral x A x B x x A x B
28 25 26 27 3bitr4i A B x A x B