Metamath Proof Explorer


Theorem rexeqbidvv

Description: Version of rexeqbidv with additional disjoint variable conditions, not requiring ax-8 nor df-clel . (Contributed by Wolf Lammen, 25-Sep-2024)

Ref Expression
Hypotheses raleqbidvv.1 ( 𝜑𝐴 = 𝐵 )
raleqbidvv.2 ( 𝜑 → ( 𝜓𝜒 ) )
Assertion rexeqbidvv ( 𝜑 → ( ∃ 𝑥𝐴 𝜓 ↔ ∃ 𝑥𝐵 𝜒 ) )

Proof

Step Hyp Ref Expression
1 raleqbidvv.1 ( 𝜑𝐴 = 𝐵 )
2 raleqbidvv.2 ( 𝜑 → ( 𝜓𝜒 ) )
3 2 adantr ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
4 1 3 rexeqbidva ( 𝜑 → ( ∃ 𝑥𝐴 𝜓 ↔ ∃ 𝑥𝐵 𝜒 ) )