Metamath Proof Explorer


Theorem rabiun

Description: Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017)

Ref Expression
Assertion rabiun x y A B | φ = y A x B | φ

Proof

Step Hyp Ref Expression
1 eliun x y A B y A x B
2 1 anbi1i x y A B φ y A x B φ
3 r19.41v y A x B φ y A x B φ
4 2 3 bitr4i x y A B φ y A x B φ
5 4 abbii x | x y A B φ = x | y A x B φ
6 df-rab x y A B | φ = x | x y A B φ
7 iunab y A x | x B φ = x | y A x B φ
8 5 6 7 3eqtr4i x y A B | φ = y A x | x B φ
9 df-rab x B | φ = x | x B φ
10 9 a1i y A x B | φ = x | x B φ
11 10 iuneq2i y A x B | φ = y A x | x B φ
12 8 11 eqtr4i x y A B | φ = y A x B | φ