| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > raleqbidv | Structured version Visualization version GIF version | ||
| Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2141, ax-11 2157, and ax-12 2177 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
| Ref | Expression |
|---|---|
| raleqbidv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| raleqbidv.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| raleqbidv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | raleqbidv.1 | . . . 4 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | 1 | eleq2d 2827 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
| 3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 4 | 2, 3 | imbi12d 344 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
| 5 | 4 | ralbidv2 3174 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
| Copyright terms: Public domain | W3C validator |