Metamath Proof Explorer


Theorem raleqbidvv

Description: Version of raleqbidv with additional disjoint variable conditions, not requiring ax-8 nor df-clel . (Contributed by BJ, 22-Sep-2024)

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

Proof

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