Metamath Proof Explorer


Theorem rexlim2d

Description: Inference removing two restricted quantifiers. Same as rexlimdvv , but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses rexlim2d.x 𝑥 𝜑
rexlim2d.y 𝑦 𝜑
rexlim2d.3 ( 𝜑 → ( ( 𝑥𝐴𝑦𝐵 ) → ( 𝜓𝜒 ) ) )
Assertion rexlim2d ( 𝜑 → ( ∃ 𝑥𝐴𝑦𝐵 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 rexlim2d.x 𝑥 𝜑
2 rexlim2d.y 𝑦 𝜑
3 rexlim2d.3 ( 𝜑 → ( ( 𝑥𝐴𝑦𝐵 ) → ( 𝜓𝜒 ) ) )
4 nfv 𝑥 𝜒
5 nfv 𝑦 𝑥𝐴
6 2 5 nfan 𝑦 ( 𝜑𝑥𝐴 )
7 nfv 𝑦 𝜒
8 3 expdimp ( ( 𝜑𝑥𝐴 ) → ( 𝑦𝐵 → ( 𝜓𝜒 ) ) )
9 6 7 8 rexlimd ( ( 𝜑𝑥𝐴 ) → ( ∃ 𝑦𝐵 𝜓𝜒 ) )
10 9 ex ( 𝜑 → ( 𝑥𝐴 → ( ∃ 𝑦𝐵 𝜓𝜒 ) ) )
11 1 4 10 rexlimd ( 𝜑 → ( ∃ 𝑥𝐴𝑦𝐵 𝜓𝜒 ) )