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 ( 𝐴𝐵 → ( ∃ 𝑥𝐴 𝜑 → ∃ 𝑥𝐵 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-ss ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
2 pm3.45 ( ( 𝑥𝐴𝑥𝐵 ) → ( ( 𝑥𝐴𝜑 ) → ( 𝑥𝐵𝜑 ) ) )
3 2 aleximi ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) → ( ∃ 𝑥 ( 𝑥𝐴𝜑 ) → ∃ 𝑥 ( 𝑥𝐵𝜑 ) ) )
4 df-rex ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥𝐴𝜑 ) )
5 df-rex ( ∃ 𝑥𝐵 𝜑 ↔ ∃ 𝑥 ( 𝑥𝐵𝜑 ) )
6 3 4 5 3imtr4g ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) → ( ∃ 𝑥𝐴 𝜑 → ∃ 𝑥𝐵 𝜑 ) )
7 1 6 sylbi ( 𝐴𝐵 → ( ∃ 𝑥𝐴 𝜑 → ∃ 𝑥𝐵 𝜑 ) )