Metamath Proof Explorer

Theorem rexbii

Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 6-Dec-2019)

Ref Expression
Hypothesis rexbii.1 φ ψ
Assertion rexbii x A φ x A ψ


Step Hyp Ref Expression
1 rexbii.1 φ ψ
2 1 anbi2i x A φ x A ψ
3 2 rexbii2 x A φ x A ψ