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 ψ

Proof

Step Hyp Ref Expression
1 rexbii.1 φ ψ
2 1 a1i x A φ ψ
3 2 rexbiia x A φ x A ψ