![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > raleq | GIF version |
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) |
Ref | Expression |
---|---|
raleq | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2319 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2319 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | raleqf 2668 | 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: raleqi 2676 raleqdv 2678 raleqbi1dv 2680 sbralie 2721 inteq 3845 iineq1 3898 bnd2 4170 frforeq2 4342 weeq2 4354 ordeq 4369 reg2exmid 4532 reg3exmid 4576 omsinds 4618 fncnv 5278 funimaexglem 5295 isoeq4 5799 acexmidlemv 5867 tfrlem1 6303 tfr0dm 6317 tfrlemisucaccv 6320 tfrlemi1 6327 tfrlemi14d 6328 tfrexlem 6329 tfr1onlemsucaccv 6336 tfr1onlemaccex 6343 tfr1onlemres 6344 tfrcllemsucaccv 6349 tfrcllembxssdm 6351 tfrcllemaccex 6356 tfrcllemres 6357 tfrcldm 6358 ixpeq1 6703 ac6sfi 6892 fimax2gtri 6895 dcfi 6974 supeq1 6979 supeq2 6982 nnnninfeq2 7121 isomni 7128 ismkv 7145 iswomni 7157 sup3exmid 8900 rexanuz 10978 rexfiuz 10979 fimaxre2 11216 modfsummod 11447 mhmpropd 12744 iscmn 12920 srgideu 12978 cnprcl2k 13366 ispsmet 13483 ismet 13504 isxmet 13505 cncfval 13719 dvcn 13824 setindis 14368 bdsetindis 14370 strcoll2 14384 strcollnfALT 14387 |
Copyright terms: Public domain | W3C validator |