Description: Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)
Ref | Expression | ||
---|---|---|---|
Assertion | abrexex2g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv | |
|
2 | nfcv | |
|
3 | nfs1v | |
|
4 | 2 3 | nfrex | |
5 | sbequ12 | |
|
6 | 5 | rexbidv | |
7 | 1 4 6 | cbvabw | |
8 | df-clab | |
|
9 | 8 | rexbii | |
10 | 9 | abbii | |
11 | 7 10 | eqtr4i | |
12 | df-iun | |
|
13 | iunexg | |
|
14 | 12 13 | eqeltrrid | |
15 | 11 14 | eqeltrid | |