Metamath Proof Explorer


Theorem iinxprg

Description: Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012)

Ref Expression
Hypotheses iinxprg.1 x=AC=D
iinxprg.2 x=BC=E
Assertion iinxprg AVBWxABC=DE

Proof

Step Hyp Ref Expression
1 iinxprg.1 x=AC=D
2 iinxprg.2 x=BC=E
3 1 eleq2d x=AyCyD
4 2 eleq2d x=ByCyE
5 3 4 ralprg AVBWxAByCyDyE
6 5 abbidv AVBWy|xAByC=y|yDyE
7 df-iin xABC=y|xAByC
8 df-in DE=y|yDyE
9 6 7 8 3eqtr4g AVBWxABC=DE