Metamath Proof Explorer


Theorem iinexg

Description: The existence of a class intersection. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by FL, 19-Sep-2011)

Ref Expression
Assertion iinexg AxABCxABV

Proof

Step Hyp Ref Expression
1 dfiin2g xABCxAB=y|xAy=B
2 1 adantl AxABCxAB=y|xAy=B
3 elisset BCyy=B
4 3 rgenw xABCyy=B
5 r19.2z AxABCyy=BxABCyy=B
6 4 5 mpan2 AxABCyy=B
7 r19.35 xABCyy=BxABCxAyy=B
8 6 7 sylib AxABCxAyy=B
9 8 imp AxABCxAyy=B
10 rexcom4 xAyy=ByxAy=B
11 9 10 sylib AxABCyxAy=B
12 abn0 y|xAy=ByxAy=B
13 11 12 sylibr AxABCy|xAy=B
14 intex y|xAy=By|xAy=BV
15 13 14 sylib AxABCy|xAy=BV
16 2 15 eqeltrd AxABCxABV