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 3111 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
3 | raleqbidva.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | raleqdv 3348 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
5 | 2, 4 | bitrd 278 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ∀wral 3064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2730 df-ral 3069 |
This theorem is referenced by: catpropd 17418 cidpropd 17419 funcpropd 17616 fullpropd 17636 natpropd 17694 gsumpropd2lem 18363 istrkgc 26815 istrkgb 26816 istrkgcb 26817 istrkge 26818 iscgrg 26873 isperp 27073 clwlkclwwlk 28366 rngurd 31482 lindfpropd 31576 ist0cld 31783 matunitlindflem1 35773 sticksstones3 40104 sticksstones11 40112 |
Copyright terms: Public domain | W3C validator |