Metamath Proof Explorer


Theorem abrexex2g

Description: Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion abrexex2g AVxAy|φWy|xAφV

Proof

Step Hyp Ref Expression
1 nfv zxAφ
2 nfcv _yA
3 nfs1v yzyφ
4 2 3 nfrex yxAzyφ
5 sbequ12 y=zφzyφ
6 5 rexbidv y=zxAφxAzyφ
7 1 4 6 cbvabw y|xAφ=z|xAzyφ
8 df-clab zy|φzyφ
9 8 rexbii xAzy|φxAzyφ
10 9 abbii z|xAzy|φ=z|xAzyφ
11 7 10 eqtr4i y|xAφ=z|xAzy|φ
12 df-iun xAy|φ=z|xAzy|φ
13 iunexg AVxAy|φWxAy|φV
14 12 13 eqeltrrid AVxAy|φWz|xAzy|φV
15 11 14 eqeltrid AVxAy|φWy|xAφV