Theorem ralbidc

Description: Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb . (Contributed by Zhi Wang, 30-Aug-2024)

	Ref	Expression
Hypotheses	ralbidb.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
	ralbidc.2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) → ( 𝜒 ↔ 𝜃 ) ) )
Assertion	ralbidc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜒 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝜓 → 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralbidb.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
2		ralbidc.2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) → ( 𝜒 ↔ 𝜃 ) ) )
3	1 2	imbi12d3	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 → 𝜒 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → 𝜃 ) ) )
4		impexp	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → 𝜃 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝜓 → 𝜃 ) ) )
5	3 4	bitrdi	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 → 𝜒 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝜓 → 𝜃 ) ) ) )
6	5	ralbidv2	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜒 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝜓 → 𝜃 ) ) )