|   | 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 3175 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | 
| 3 | raleqbidva.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 4 | 3 | raleqdv 3325 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | 
| 5 | 2, 4 | bitrd 279 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-ral 3061 df-rex 3070 | 
| This theorem is referenced by: raleqbidvv 3333 catpropd 17753 cidpropd 17754 funcpropd 17948 fullpropd 17968 natpropd 18025 gsumpropd2lem 18693 ringurd 20183 istrkgcb 28465 iscgrg 28521 isperp 28721 clwlkclwwlk 30022 urpropd 33237 domnpropd 33281 lindfpropd 33411 opprqus0g 33519 opprqusdrng 33522 ist0cld 33833 matunitlindflem1 37624 primrootsunit1 42099 sticksstones3 42150 | 
| Copyright terms: Public domain | W3C validator |