Metamath Proof Explorer


Theorem rexxfr3d

Description: Transfer existential quantification from a variable x to another variable y contained in expression A . (Contributed by SN, 20-Jun-2025)

Ref Expression
Hypotheses rexxfr3d.s ( 𝑥 = 𝑋 → ( 𝜓𝜒 ) )
rexxfr3d.x ( 𝜑 → ( 𝑥𝐴 ↔ ∃ 𝑦𝐵 𝑥 = 𝑋 ) )
rexxfr3d.a ( 𝜑𝑋𝑉 )
Assertion rexxfr3d ( 𝜑 → ( ∃ 𝑥𝐴 𝜓 ↔ ∃ 𝑦𝐵 𝜒 ) )

Proof

Step Hyp Ref Expression
1 rexxfr3d.s ( 𝑥 = 𝑋 → ( 𝜓𝜒 ) )
2 rexxfr3d.x ( 𝜑 → ( 𝑥𝐴 ↔ ∃ 𝑦𝐵 𝑥 = 𝑋 ) )
3 rexxfr3d.a ( 𝜑𝑋𝑉 )
4 3 adantr ( ( 𝜑𝑦𝐵 ) → 𝑋𝑉 )
5 1 adantl ( ( 𝜑𝑥 = 𝑋 ) → ( 𝜓𝜒 ) )
6 4 2 5 rexxfr2d ( 𝜑 → ( ∃ 𝑥𝐴 𝜓 ↔ ∃ 𝑦𝐵 𝜒 ) )