![]() |
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 3174 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
3 | raleqbidva.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | raleqdv 3324 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
5 | 2, 4 | bitrd 279 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1540 ∈ wcel 2105 ∀wral 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-cleq 2723 df-ral 3061 df-rex 3070 |
This theorem is referenced by: raleqbidvv 3328 catpropd 17658 cidpropd 17659 funcpropd 17856 fullpropd 17876 natpropd 17934 gsumpropd2lem 18605 ringurd 20080 istrkgcb 27975 iscgrg 28031 isperp 28231 clwlkclwwlk 29523 urpropd 32649 lindfpropd 32773 opprqus0g 32879 opprqusdrng 32882 ist0cld 33112 matunitlindflem1 36788 sticksstones3 41271 sticksstones11 41279 |
Copyright terms: Public domain | W3C validator |