Description: Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ralbidb.1 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) | |
| ralbidb.2 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜒 ↔ 𝜃 ) ) | ||
| Assertion | ralbidb | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜒 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝜓 → 𝜃 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralbidb.1 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) | |
| 2 | ralbidb.2 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜒 ↔ 𝜃 ) ) | |
| 3 | 1 2 | logic1a | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 → 𝜒 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → 𝜃 ) ) ) |
| 4 | impexp | ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → 𝜃 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝜓 → 𝜃 ) ) ) | |
| 5 | 3 4 | bitrdi | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 → 𝜒 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝜓 → 𝜃 ) ) ) ) |
| 6 | 5 | ralbidv2 | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜒 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝜓 → 𝜃 ) ) ) |