Description: Split a biconditional and distribute two restricted universal quantifiers, analogous to 2albiim and ralbiim . (Contributed by Alexander van der Vekens, 2-Jul-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 2ralbiim | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralbiim | ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜑 ) ) ) | |
| 2 | 1 | ralbii | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 ↔ 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜑 ) ) ) |
| 3 | r19.26 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜑 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜑 ) ) ) | |
| 4 | 2 3 | bitri | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜑 ) ) ) |