Theorem reueqbidva

Description: Formula-building rule for restricted existential uniqueness quantifier. Deduction form. General version of reueqbidv . (Contributed by Zhi Wang, 20-Nov-2025)

	Ref	Expression
Hypotheses	reueqbidva.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	reueqbidva.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	reueqbidva	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑥 ∈ 𝐵 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		reueqbidva.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		reueqbidva.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
3	2	reubidva	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑥 ∈ 𝐴 𝜒 ) )
4	1	reueqdv	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐴 𝜒 ↔ ∃! 𝑥 ∈ 𝐵 𝜒 ) )
5	3 4	bitrd	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑥 ∈ 𝐵 𝜒 ) )