Metamath Proof Explorer


Theorem mnuss2d

Description: mnussd with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuss2d.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
mnuss2d.2 φ U M
mnuss2d.3 φ x U A x
Assertion mnuss2d φ A U

Proof

Step Hyp Ref Expression
1 mnuss2d.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
2 mnuss2d.2 φ U M
3 mnuss2d.3 φ x U A x
4 2 adantr φ x U A x U M
5 simprl φ x U A x x U
6 simprr φ x U A x A x
7 1 4 5 6 mnussd φ x U A x A U
8 3 7 rexlimddv φ A U