Description: Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii . (Contributed by David A. Wheeler, 21-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | alseubii.1 | ⊢ ( 𝜑 ↔ 𝜒 ) | |
| alseubii.2 | ⊢ ( 𝜓 ↔ 𝜃 ) | ||
| Assertion | alseubii | ⊢ ( ∀∃! 𝑥 ( 𝜑 → 𝜓 ) ↔ ∀∃! 𝑥 ( 𝜒 → 𝜃 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alseubii.1 | ⊢ ( 𝜑 ↔ 𝜒 ) | |
| 2 | alseubii.2 | ⊢ ( 𝜓 ↔ 𝜃 ) | |
| 3 | 1 2 | imbi12i | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜒 → 𝜃 ) ) |
| 4 | 3 | albii | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ( 𝜒 → 𝜃 ) ) |
| 5 | 1 | eubii | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜒 ) |
| 6 | 4 5 | anbi12i | ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ( 𝜒 → 𝜃 ) ∧ ∃! 𝑥 𝜒 ) ) |
| 7 | df-alseu | ⊢ ( ∀∃! 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 𝜑 ) ) | |
| 8 | df-alseu | ⊢ ( ∀∃! 𝑥 ( 𝜒 → 𝜃 ) ↔ ( ∀ 𝑥 ( 𝜒 → 𝜃 ) ∧ ∃! 𝑥 𝜒 ) ) | |
| 9 | 6 7 8 | 3bitr4i | ⊢ ( ∀∃! 𝑥 ( 𝜑 → 𝜓 ) ↔ ∀∃! 𝑥 ( 𝜒 → 𝜃 ) ) |