Metamath Proof Explorer


Theorem rabrabi

Description: Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022) Avoid ax-10 , ax-11 and ax-12 . (Revised by Gino Giotto, 12-Oct-2024)

Ref Expression
Hypothesis rabrabi.1 x = y χ φ
Assertion rabrabi x y A | φ | ψ = x A | χ ψ

Proof

Step Hyp Ref Expression
1 rabrabi.1 x = y χ φ
2 df-rab y A | φ = y | y A φ
3 2 eleq2i x y A | φ x y | y A φ
4 df-clab x y | y A φ x y y A φ
5 eleq1w y = x y A x A
6 1 bicomd x = y φ χ
7 6 equcoms y = x φ χ
8 5 7 anbi12d y = x y A φ x A χ
9 8 sbievw x y y A φ x A χ
10 4 9 bitri x y | y A φ x A χ
11 3 10 bitri x y A | φ x A χ
12 11 anbi1i x y A | φ ψ x A χ ψ
13 anass x A χ ψ x A χ ψ
14 12 13 bitri x y A | φ ψ x A χ ψ
15 14 rabbia2 x y A | φ | ψ = x A | χ ψ