Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > raleqbidva | Structured version Visualization version GIF version |
Description: Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
Ref | Expression |
---|---|
raleqbidva.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
raleqbidva.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
raleqbidva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleqbidva.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
2 | 1 | ralbidva 2968 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
3 | raleqbidva.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | raleqdv 3121 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
5 | 2, 4 | bitrd 267 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 |
This theorem is referenced by: catpropd 16192 cidpropd 16193 funcpropd 16383 fullpropd 16403 natpropd 16459 gsumpropd2lem 17096 istrkgc 25153 istrkgb 25154 istrkgcb 25155 istrkge 25156 iscgrg 25207 isperp 25407 clwlkisclwwlk 26317 rngurd 29119 matunitlindflem1 32575 clwlkclwwlk 41211 |
Copyright terms: Public domain | W3C validator |