![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > raleqbidv | GIF version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) |
Ref | Expression |
---|---|
raleqbidv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
raleqbidv.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
raleqbidv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleqbidv.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | raleqdv 2678 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 3 | ralbidv 2477 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
5 | 2, 4 | bitrd 188 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1353 ∀wral 2455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 |
This theorem is referenced by: rspc2vd 3125 ofrfval 6090 fmpox 6200 tfrlemi1 6332 supeq123d 6989 cvg1nlemcau 10988 cvg1nlemres 10989 cau3lem 11118 fsum2dlemstep 11437 fisumcom2 11441 fprod2dlemstep 11625 fprodcom2fi 11629 pcfac 12342 ptex 12707 prdsex 12712 ismgm 12770 mgm1 12783 grpidvalg 12786 issgrp 12803 sgrp1 12810 ismnddef 12813 ismndd 12832 mndpropd 12835 mnd1 12841 ismhm 12847 isgrp 12877 grppropd 12887 isgrpd2e 12890 grp1 12970 isnsg 13055 nmznsg 13066 cmnpropd 13091 iscmnd 13094 dfur2g 13138 issrg 13141 issrgid 13157 isring 13176 iscrng2 13191 ringideu 13193 isringid 13201 ringpropd 13210 ring1 13229 oppr0g 13244 oppr1g 13245 islring 13326 istopg 13430 restbasg 13599 cnfval 13625 cnpfval 13626 txbas 13689 limccl 14059 sscoll2 14660 |
Copyright terms: Public domain | W3C validator |