![]() |
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 2223 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2223 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | raleqf 2550 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 = wceq 1285 ∀wral 2353 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 |
This theorem is referenced by: raleqi 2558 raleqdv 2560 raleqbi1dv 2562 sbralie 2595 inteq 3659 iineq1 3712 bnd2 3967 frforeq2 4128 weeq2 4140 ordeq 4155 reg2exmid 4307 reg3exmid 4350 fncnv 5016 funimaexglem 5033 isoeq4 5496 acexmidlemv 5562 tfrlem1 5978 tfr0dm 5992 tfrlemisucaccv 5995 tfrlemi1 6002 tfrlemi14d 6003 tfrexlem 6004 tfr1onlemsucaccv 6011 tfr1onlemaccex 6018 tfr1onlemres 6019 tfrcllemsucaccv 6024 tfrcllembxssdm 6026 tfrcllemaccex 6031 tfrcllemres 6032 tfrcldm 6033 ac6sfi 6455 supeq1 6494 supeq2 6497 rexanuz 10093 rexfiuz 10094 fimaxre2 10328 setindis 11047 bdsetindis 11049 strcoll2 11063 |
Copyright terms: Public domain | W3C validator |