Metamath Proof Explorer


Theorem ssrexv

Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007) Avoid axioms. (Revised by GG, 19-May-2025)

Ref Expression
Assertion ssrexv A B x A φ x B φ

Proof

Step Hyp Ref Expression
1 df-ss A B x x A x B
2 pm3.45 x A x B x A φ x B φ
3 2 aleximi x x A x B x x A φ x x B φ
4 df-rex x A φ x x A φ
5 df-rex x B φ x x B φ
6 3 4 5 3imtr4g x x A x B x A φ x B φ
7 1 6 sylbi A B x A φ x B φ